Abstract
The vision of machines autonomously carrying out substantive conjecture generation, theorem discovery, proof discovery, and proof verification in mathematics and the natural sciences has a long history that reaches back before the development of automatic systems designed for such processes. While there has been considerable progress in proof verification in the formal sciences, for instance the Mizar project’ and the four-color theorem, now machine verified, there has been scant such work carried out in the realm of the natural sciences—until recently. The delay in the case of the natural sciences can be attributed to both a lack of formal analysis of the so-called “theories” in such sciences, and the lack of sufficient progress in automated theorem proving. While the lack of analysis is probably due to an inclination toward informality and empiricism on the part of nearly all of the relevant scientists, the lack of progress is to be expected, given the computational hardness of automated theorem proving; after all, theoremhood in even first-order logic is Turing-undecidable. We give in the present short paper a compressed report on our building upon these formal theories using logic-based AI in order to achieve, in relativity, both machine proof discovery and proof verification, for theorems previously established by humans. Our report is intended to serve as a springboard to machine-produced results in the future that have not been obtained by humans.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
We take this to be a temporally ordered four-stage sequence, which starts with generation of statements that may be theorems (and are usually interesting in their own right), proceeds to grasping that it’s at least a very good bet that one or more such statements is/are indeed (a) theorem(s) (those that aren’t theorems can of course eventually end up as theorems in a sense, if their negations are established), then moves to finding a proof of these statements, and concludes with a verification of said proof.
One could in fact argue that Aristotle, over two thousand years back, intuitively had, and indeed pursued, the vision: See the discussion of Aristotle in connection with modern knowledge-based AI given by Glymour (1992). And as is well-known, Leibniz certainly seems to have had some such vision, in connection with his spécieuse générale; indeed he had not only the idea of knowledge representation in todays’s field of AI, but also of computation over this knowledge. Interested readers can consult (Couturat 1901).
Masterful coverage of multi-sorted FOL is provided by (Manzano 1996).
Note that we differentiate local assumptions, which may discharged and introduced frequently, versus global axioms and premises, which are always taken to be true. This distinction is more for convenience than for any deep, principled reason at this point.
Slate is under active development. To obtain the most recent version of Slate, please contact the authors directly. For an overview of an earlier version of Slate, see Bringsjord et al. (2008).
The identifiers move Slate outside of the usual “block” structure of natural deduction, and allow the machine to intelligently serve as an informative assistant. In the modal case, Slate assists the user by informing her that for instance iterated modal operators are permissible with respect to a given formula node.
A bigger version of the manual proof can be obtained at https://s3.amazonaws.com/SyntheseSubmission/Theorem_no_event_at_two_place_manual.pdf.
Fig. 2 
Semi-automated slate proof of NEAT and Speed2
Fig. 3 
Resolution and paramodulation slate proofs of NEAT and Speed2
Fig. 4 
Manual proof in slate of NEAT
For reasons of convenience, we switch between considering the speed of light to be the same constant for all observers and an observer-dependent constant. Proofs of either kind can be easily converted to the other.
The code for the whole proof in the semi-automated layer can be obtained at this url: https://s3.amazonaws.com/SyntheseSubmission/logicphysics.zip.
Fig. 5 
Partial semi-automated proof tree for Theorem NTFL branch 2
Fig. 6 
Exploded nodes of the partial semi-automated proof tree for Theorem NTFL branch 2
Fig. 7 
Semi-automated proof tree for Theorem NTFL branch 3
Fig. 8 
Exploded nodes of the semi-automated proof tree for Theorem NTFL branch 3
The criterion for distinguishing diagrammatic representations from symbolic representations is that the former are homomorphic in some fashion to what is being represented; see Barwise and Etchemendy (1995) for a discussion of this form of representation, versus linguistic/symbolic representations. The distinction is discussed in the context of logic-based AI and computational logic generally (Arkoudas and Bringsjord 2009b). Alert readers will have noticed our reference to Leibniz in footnote 2. It’s worth mentioning that Leibniz’ vision for a universal logic was not that this logic be linguistic/symbolic only, but homomorphic; this is obvious from even Leibniz’ doctoral dissertation, De Arte Combinatoria.
Fig. 9 
Example of Diagrammatic Reasoning in Physics (Andréka et al. 2007). A common pattern in special relativity is to consider situations involving a spaceship and a stationary observer. Here, we have two photons, \(\mathsf {Ph3}\) and \(\mathsf {Ph4}\), emitted from the middle of the ship toward mirrors on its opposite ends. If the speed of light is constant for all observers, we can immediately see that the times taken by both the photons for their roundtrip are the same
Fig. 10 
Geometric Reasoning Using Diagrams from (Andréka et al. 2011). This figure is a part of the informal proof of Theorem NFTL. In the left half of the figure, we assume that there are two spacetime points \(x\) and \(y\) at which \(m\) sees \(k\), with the speed of \(k\) as seen by \(m\) being greater than the speed of light. With some simple reasoning, we deduce that there is a point \(w\) on the plane of \(xyz\), such that lines \(wz\) and \(wy\) are parallel. This is a contradiction, as \(w\) cannot exist!
References
Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., & Owre, S. (2001). Computer algebra meets automated theorem proving: Integrating Maple and PVS. Theorem proving in higher order logics (pp. 27–42). Heidelberg: Springer.
Andréka, H., Madarász, J. X., & Németi, I. (2002). On the logical structure of relativity theories, Alfréd Rényi Institute of Mathematics. With contributions from A. Andai, G. Sági, I. Sain, & Cs. Töke. http://www.math-inst.hu/pub/algebraic-logic/olsort.html. Accessed 2 April 2014.
Andréka, H., Madarász, J. X., & Németi, I. (2007). Logic of space-time and relativity theory. In M. Aiello, I. Pratt-Hartmann, & J. van Benthem (Eds.), Handbook of spatial logics (pp. 607–711). Dordrecht: Springer.
Andréka, H., Madarász, J. X., Németi, I., & Székely, G. (2011). A logic road from special relativity to general relativity, Synthese (pp. 1–17). http://dx.doi.org/10.1007/s11229-011-9914-8. Accessed 2 April 2014.
Arkoudas, K. (2000). Denotational Proof Languages, Ph.D. Thesis, MIT.
Arkoudas, K. (2005). Combining diagrammatic and symbolic reasoning, Technical Report 2005–59. MIT Computer Science and Artificial Intelligence Lab, Cambridge, USA
Arkoudas, K. & Bringsjord, S. (2007). Computers, justification, and mathematical knowledge. Minds and Machines 17(2), 185–202. http://kryten.mm.rpi.edu/ka_sb_proofs_offprint.pdf. Accessed 2 April 2014.
Arkoudas, K. & Bringsjord, S. (2009a). Propositional attitudes and causation. International Journal of Software and Informatics 3(1), 47–65. http://kryten.mm.rpi.edu/PRICAI_w_sequentcalc_041709.pdf. Accessed 2 April 2014.
Arkoudas, K. & Bringsjord, S. (2009b). Vivid: An AI framework for heterogeneous problem solving. Artificial Intelligence 173(15), 1367–1405. http://kryten.mm.rpi.edu/vivid/vivid.pdf provides a preprint of the penultimate draft only. If for some reason it is not working, please contact either author directly by email. http://kryten.mm.rpi.edu/vivid_030205.pdf. Accessed 2 April 2014.
Barwise, J., & Etchemendy, J. (1995). Heterogeneous logic. In J. Glasgow, N. Narayanan, & B. Chandrasekaran (Eds.), Diagrammatic reasoning: Cognitive and computational perspectives (pp. 211–234). Cambridge, MA: MIT Press.
Boolos, G. S., Burgess, J. P., & Jeffrey, R. C. (2003). Computability and logic (4th ed.). Cambridge, UK: Cambridge University Press.
Bringsjord, S., & Govindarajulu, N. S. (2011). In defense of the unprovability of the church-turing thesis. Journal of Unconventional Computing, 6, 353–373. Preprint available at the url given here. http://kryten.mm.rpi.edu/SB_NSG_CTTnotprovable_091510.pdf. Accessed 2 April 2014.
Bringsjord, S., Taylor, J., Shilliday, A., Clark, & M. Arkoudas, K. (2008). Slate: An argument-centered intelligent assistant to human reasoners. In F. Grasso, N. Green, R. Kibble & C. Reed (Eds.), Proceedings of the 8th International Workshop on Computational Models of Natural Argument (CMNA 8), Patras, Greece (pp. 1–10). http://kryten.mm.rpi.edu/Bringsjord_etal_Slate_cmna_crc_061708.pdf. Accessed 2 April 2014.
Couturat, L. (1901). La Logique de Leibniz. Paris, FR: Felix Alcan.
Ebbinghaus, H. D., Flum, J., & Thomas, W. (1994). Mathematical logic (2nd ed.). New York: Springer.
Glymour, C. (1992). Thinking things through. Cambridge, MA: MIT Press.
Khandelwal, A. (2013). Furthering the Continuous-change Event Calculus: Providing for Efficient Description of Additive Effects and an Automated Reasoner, Ph.D. Thesis, Rensselaer Polytechnic Institute.
Kolmogorov, A., & Uspenskii, V. (1958). On the definition of an algorithm. Uspekhi Matematicheskikh Nauk, 13(4), 3–28.
Madarász, J. X. (2002), Logic and Relativity (in the light of definability theory), Ph.D. Thesis, Eötvös Loránd University, Budapest, Hungary.
Manzano, M. (1996). Extensions of first order logic. Cambridge: Cambridge University Press.
Naumowicz, A., & Korniłowicz, A. (2009). A brief overview of Mizar. In S. Berghofer, T. Nipkow, C. Urban & M. Wenzel (Eds.), Theorem proving in higher order logics, Vol. 5674 of Lecture Notes in Computer Science (pp. 67–72). Berlin: Springer. http://dx.doi.org/10.1007/978-3-642-03359-9_5. Accessed 2 April 2014.
Smith, B., Ashburner, M., Rosse, C., Bard, J., Bug, W., Ceusters, W., et al. (2007). The OBO foundry: Coördinated evolution of ontologies to support biomedical data integration. Nature Biotechnology, 25(11), 1251–1255.
Stannett, M., & Németi, I. (2012). Using isabelle to verify special relativity, with application to hypercomputation theory, CoRR abs/1211.6468.
Stickel, M. E. (2008). SNARK - SRI’s New Automated Reasoning Kit SNARK. http://www.ai.sri.com/~stickel/snark.html. Accessed 2 April 2014.
Székely, G. (2009). First-Order Logic Investigation of Relativity Theory with an Emphasis on Accelerated Observers, Ph.D. Thesis, Eötvös Loránd University, Budapest, Hungary.
Wolfram, S. (2003). The mathematica book (5th ed.). Champaign, IL: Wolfram-Media.
Woodger, J. H., & Tarski, A. (1937). The axiomatic method in biology. Cambridge: The University Press.
Acknowledgments
We are deeply grateful for support received from both the John Templeton Foundation and the Air Force Office of Scientific Research, and acknowledge as well a deep intellectual debt to the seminal logico-mathematico-philosophical initiatives in theoretical physics at the Rényi Institute of Mathematics, which have provided a footfhold for advancing our vision of intelligent “scientist-like” machines.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Govindarajalulu, N.S., Bringsjord, S. & Taylor, J. Proof verification and proof discovery for relativity. Synthese 192, 2077–2094 (2015). https://doi.org/10.1007/s11229-014-0424-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11229-014-0424-3