Abstract

n this paper, we report our first experiments in using learning-assisted automated reasoning for the formal analysis of physical systems. In particular, we investigate the performance of automated proofs as compared to interactive ones done in HOL for the verification of ray and electromagnetic optics. Apart from automation, we also provide brief initial exploration of more general issues in formalization of physics, such as its presentation and foundations.

BibTeX

@inproceedings{CKJUUSSKCDST-CICM15,
  author    = "Cezary Kaliszyk and Josef Urban and Umair Siddique and Sanaz
               Khan Afshar and Cvetan Dunchev and Sofi{\`{e}}ne Tahar",
  title     = "Formalizing Physics: Automation, Presentation and Foundation
               Issues",
  booktitle = "Proceedings of the 8th Conference on Intelligent Computer
               Mathematics  (CICM 2015)",
  editor    = "Manfred Kerber and Jacques Carette and Cezary Kaliszyk and
               Florian Rabe and Volker Sorge",
  series    = "Lecture Notes in Computer Science",
  volume    = 9150,
  pages     = "288--295",
  year      = 2015,
  doi       = "10.1007/978-3-319-20615-8_19"
}