Abstract
We present a system of first order logic, together with soundness and completeness proofs wrt. standard first order semantics. Proofs are mechanised in Isabelle/HOL. Our definitions are computable, allowing us to derive an algorithm to test for first order validity. This algorithm may be executed in Isabelle/HOL using the rewrite engine. Alternatively the algorithm has been ported to OCaML.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
The archive of formal proofs, http://afp.sourceforge.net/
Avron, A.: Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning 10(2), 265–281 (1993)
Stefan Berghofer. Formalising first order logic in isabelle (2002) http://www4.in.tum.de/~streckem/Admin/club2_berghofer_model_theory.pdf .
Caldwell, J.: Intuitionisitic tableau extracted. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 82–96. Springer, Heidelberg (1999), http://www.nuprl.org/documents/Caldwell/tableaux99.html
Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, (1995), Available on the Web as http://www.cl.cam.ac.uk/users/jrh/papers/reflect.dvi.gz
Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 153–170. Springer, Heidelberg (1998)
Henkin, L.: The completeness of the first-order functional calculus. The Journal of Symbolic Logic 14, 159–166 (1949)
Margetson, J.: Completeness of the first order predicate calculus, Unpublished description of formalisation in Isabelle/HOL of [WW92] (1999)
McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. Journal of Automated Reasoning 23(3–4) (November 1999)
Persson, H.: Constructive completeness of intuitionistic predicate logic (1996), http://www.cs.chalmers.se/Cs/Research/Logic/publications.mhtml
Pfenning, F.: Structural cut elimination I. intuitionistic and classical logic. Information and Computation 157(1/2), 84–141 (2000)
Pollack, R.: A verified typechecker. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902. Springer, Heidelberg (1995)
Van Orman Quine, W.: Mathematical Logic. Harper and Row (1962)
Ridge, T.: Informatics homepage. http://homepages.inf.ed.ac.uk/s0128214/
Shankar, N.: Metamathematics, Machines, and Gödel’s Proof. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1994), http://www.csl.sri.com/users/shankar/goedel-book.html
Melham, T.F.: The HOL logic extended with quantification over type variables. In: Claesen, L.J.M., Gordon, M.J.C. (eds.) International Workshop on Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium, pp. 3–18. North-Holland, Amsterdam (1992)
Underwood, J.: Tableau for intuitionistic predicate logic as metatheory. In: Baumgartner, P., Posegga, J., Hähnle, R. (eds.) TABLEAUX 1995. LNCS, vol. 918. Springer, Heidelberg (1995), http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-321/
Weich, K.: Improving Proof Search in Intuitionistic Propositional Logic. Logos-Verlag (2001), http://www.logos-verlag.de/cgi-bin/engbuchmid?isbn=767&lng=eng&id=
Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 305–320. Springer, Heidelberg (2004)
Wainer, S.S., Wallen, L.A.: Basic proof theory. In: Wainer, S.S., Aczel, P., Simmons, H. (eds.) Proof Theory: A Selection of Papers from the Leeds Proof Theory Programme 1990, pp. 3–26. Cambridge University Press, Cambridge (1992)
Zach, R., Tennant, N., Avron, A., Kremer, M., Parsons, C., Chow, T.Y.: The rule of generalization in fol, and pseudo-theorems. Thread on the FOM mailing list, http://www.cs.nyu.edu/pipermail/fom/2004-September/008513.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ridge, T., Margetson, J. (2005). A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_19
Download citation
DOI: https://doi.org/10.1007/11541868_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28372-0
Online ISBN: 978-3-540-31820-0
eBook Packages: Computer ScienceComputer Science (R0)