nach oben

Journal of Automated Reasoning

Erschienen in:

20.01.2018

Formalization of the Resolution Calculus for First-Order Logic

verfasst von: Anders Schlichtkrull

Erschienen in: Journal of Automated Reasoning | Ausgabe 1-4/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations and semantic trees. The correspondence between unsatisfiable sets of clauses and finite semantic trees is formalized in Herbrand’s theorem. I discuss the difficulties that I had formalizing proofs of the lifting lemma found in the literature, and I formalize a correct proof. The completeness proof is by induction on the size of a finite semantic tree. Throughout the paper I emphasize details that are often glossed over in paper proofs. I give a thorough overview of formalizations of first-order logic found in the literature. The formalization of resolution is part of the IsaFoL project, which is an effort to formalize logics in Isabelle/HOL.

Vorheriger Artikel Hammer for Coq: Automation for Dependent Type Theory

Nächster Artikel Formally Verified Algorithms for Upper-Bounding State Space Diameters

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Anderson, R., Bledsoe, W.W.: A linear format for resolution with merging and a new technique for establishing completeness. J. ACM 17(3), 525–534 (1970)MathSciNetCrossRefMATH

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefMATH

Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of Knuth–Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Lambda_Free_KBOs.shtml, Formal proof development

Ben-Ari, M.: Mathematical Logic for Computer Science, 3rd edn. Springer, New York (2012)CrossRefMATH

Berghofer, S.: First-order logic according to Fitting. Archive of Formal Proofs (2007). http://isa-afp.org/entries/FOL-Fitting.shtml, Formal proof development

Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)MathSciNetCrossRefMATH

Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 25–44. Springer, New York (2016)

Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 93–110. Springer, New York (2014)

Blanchette, J.C., Popescu, A., Traytel, D.: Abstract completeness. Archive of Formal Proofs (2014). http://isa-afp.org/entries/Abstract_Completeness.shtml, Formal proof development

10.

Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: Fisher, K., Reppy, J. (eds.) ICFP’15, pp. 192–204. ACM (2015)

11.

Blanchette, J.C., Popescu, A., Traytel, D.: Abstract soundness. Archive of Formal Proofs (2017). http://isa-afp.org/entries/Abstract_Soundness.shtml, Formal proof development

12.

Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149–179 (2017)MathSciNetCrossRefMATH

13.

Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of recursive path orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Lambda_Free_RPOs.shtml, Formal proof development

14.

Braselmann, P., Koepke, P.: Gödel completeness theorem. Formaliz. Math. 13(1), 49–53 (2005)

15.

Braselmann, P., Koepke, P.: A sequent calculus for first-order logic. Formaliz. Math. 13(1), 33–39 (2005)

16.

Breitner, J.: Visual theorem proving with the Incredible Proof Machine. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807, pp. 123–139. Springer, New York (2016)

17.

Breitner, J., Lohner, D.: The meta theory of the Incredible Proof Machine. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Incredible_Proof_Machine.shtml, Formal proof development

18.

Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE-9, LNCS, vol. 310, pp. 111–120. Springer, New York (1988)

19.

Chang, C.L., Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving, 1st edn. Academic Press, Cambridge (1973)MATH

20.

Coen, M., Slind, K., Krauss, A.: Theory unification. Isabelle. http://isabelle.in.tum.de/library/HOL/HOL-ex/Unification.html. Accessed 13 Dec 2017

21.

Coen, M.D.: Interactive program derivation. Ph.D. thesis, University of Cambridge (1992). http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-272.html

22.

Corbin, J., Bidoit, M.: A rehabilitation of Robinson’s unification algorithm. In: IFIP Congress, pp. 909–914 (1983)

23.

Davis, J., Myreen, M.O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it). J. Autom. Reason. (2015)

24.

Ebbinghaus, H., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Springer, New York (1994)CrossRefMATH

25.

Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996). Second EditionCrossRefMATH

26.

Gebhard, H.: Beweisplanung für die Beweise der Vollständigkeit verschiedener Resolutionskalküle in \(\rm \Omega \it \) MEGA. Master’s thesis, Saarland University (1999)

27.

Goubault-Larrecq, J., Jouannaud, J.P.: The blossom of finite semantic trees. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics: Essays in Memory of Harald Ganzinger, LNCS, pp. 90–122. Springer, New York (2013)CrossRef

28.

Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOL’s 1998, LNCS, vol. 1497, pp. 153–170. Springer, New York (1998)

29.

Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006, LNCS, vol. 4130, pp. 177–191. Springer, New York (2006)

30.

Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)CrossRefMATH

31.

Ilik, D.: Constructive completeness proofs and delimited control. Ph.D. thesis, École Polytechnique (2010). https://tel.archives-ouvertes.fr/tel-00529021/document

32.

Ilik, D., Lee, G., Herbelin, H.: Kripke models for classical logic. Ann. Pure Appl. Log. 161(11), 1367–1378 (2010)MathSciNetCrossRefMATH

33.

IsaFoL authors: IsaFoL: Isabelle Formalization of Logic. https://bitbucket.org/isafol/isafol. Accessed 13 Dec 2017

34.

IsaFoR developers: An Isabelle/HOL formalization of rewriting for certified termination analysis. http://cl-informatik.uibk.ac.at/software/ceta/. Accessed 13 Dec 2017

35.

Jensen, A.B., Schlichtkrull, A., Villadsen, J.: Verification of an LCF-style first-order prover with equality. In: Isabelle Workshop 2016 Associated with ITP 2016 (2016)

36.

Jensen, A.B., Schlichtkrull, A., Villadsen, J.: First-order logic according to Harrison. Archive of Formal Proofs (2017). http://isa-afp.org/entries/FOL_Harrison.shtml, Formal proof development

37.

Kohlhase, M.: Theorem prover museum – OMEGA theories – folders: propositional-logic, resolution, proof-theory, prop-res. https://github.com/theoremprover-museum/OMEGA/tree/master/theories. Accessed 13 Dec 2017

38.

Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303–336 (2010)MathSciNetCrossRefMATH

39.

Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: Self-formalisation of higher-order logic: semantics, soundness, and a verified implementation. J. Autom. Reason. 56(3), 221–259 (2016)MathSciNetCrossRefMATH

40.

Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE-26, LNCS, vol. 10395, pp. 237–254. Springer, New York (2017)

41.

Lammich, P.: The GRAT tool chain. In: Gaspers, S., Walsh, T. (eds.) SAT 2017, LNCS, vol. 10491, pp. 457–463. Springer, New York (2017)

42.

Leitsch, A.: On different concepts of resolution. Math. Log. Q. 35(1), 71–77 (1989)MathSciNetCrossRefMATH

43.

Leitsch, A.: The Resolution Calculus. Springer, New York (1997)CrossRefMATH

44.

Manna, Z., Waldinger, R.: Deductive synthesis of the unification algorithm. Sci. Comput. Program. 1(1), 5–48 (1981)MathSciNetCrossRefMATH

45.

Margetson, J., Ridge, T.: Completeness theorem. Archive of Formal Proofs (2004). http://isa-afp.org/entries/Completeness.shtml, Formal proof development

46.

Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer, New York (2014)CrossRefMATH

47.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Springer, New York (2002)MATH

48.

Paulson, L.C.: Verifying the unification algorithm in LCF. Sci. Comput. Program. 5(2), 143–169 (1985)MathSciNetCrossRefMATH

49.

Paulson, L.C.: Gödel’s incompleteness theorems. Archive of Formal Proofs (2013). http://isa-afp.org/entries/Incompleteness.shtml, Formal proof development

50.

Paulson, L.C.: A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Rev. Symb. Log. 7(03), 484–498 (2014)MathSciNetCrossRefMATH

51.

Paulson, L.C.: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. J. Autom. Reason. 55(1), 1–37 (2015)CrossRefMATH

52.

Peltier, N.: Propositional resolution and prime implicates generation. Archive of Formal Proofs (2016). http://isa-afp.org/entries/PropResPI.shtml, Formal proof development

53.

Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs (2016). http://isa-afp.org/entries/SuperCalc.shtml, Formal proof development

54.

Persson, H.: Constructive completeness of intuitionistic predicate logic. Ph.D. thesis, Chalmers University of Technology (1996). http://web.archive.org/web/19970715002824/http://www.cs.chalmers.se/~henrikp/Lic/

55.

Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning, vol. 2, pp. 1853–1964 (2001)

56.

Raffalli, C.: Krivine’s abstract completeness proof for classical predicate logic. https://github.com/craff/phox/blob/master/examples/complete.phx (2005, possibly earlier). Accessed 13 Dec 2017

57.

Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) CADE-16, LNCS, vol. 1632, pp. 292–296. Springer, New York (1999)

58.

Ridge, T.: A mechanically verified, efficient, sound and complete theorem prover for first order logic. Archive of Formal Proofs (2004). http://isa-afp.org/entries/Verified-Prover.shtml, Formal proof development

59.

Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOL’s 2005, LNCS, vol. 3603, pp. 294–309. Springer, New York (2005)

60.

Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)MathSciNetCrossRefMATH

61.

Robinson, J.A.: The generalized resolution principle. Mach. Intell. 3, 77–93 (1968)MATH

62.

Ruiz-Reina, J.L., Martín-Mateos, F.J., Alonso, J.A., Hidalgo, M.J.: Formal correctness of a quadratic unification algorithm. J. Autom. Reason. 37(1), 67–92 (2006)MathSciNetMATH

63.

Schlichtkrull, A.: Formalization of resolution calculus in Isabelle. Master’s thesis, Technical University of Denmark (2015). https://people.compute.dtu.dk/andschl/Thesis.pdf

64.

Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807, pp. 341–357. Springer, New York (2016)

65.

Schlichtkrull, A.: The resolution calculus for first-order logic. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Resolution_FOL.shtml, Formal proof development

66.

Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of Bachmair and Ganzinger’s simple ordered resolution prover. https://bitbucket.org/isafol/isafol/src/master/Ordered_Resolution_Prover/. Accessed 13 Dec 2017

67.

Schlichtkrull, A., Villadsen, J.: Paraconsistency. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Paraconsistency.shtml, Formal proof development

68.

Schlöder, J.J., Koepke, P.: The Gödel completeness theorem for uncountable languages. Formaliz. Math. 20(3), 199–203 (2012)MATH

69.

Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19, LNCS, vol. 8312, pp. 735–743. Springer, New York (2013)

70.

Shankar, N.: Proof-checking metamathematics. Ph.D. thesis, University of Texas (1986)

71.

Shankar, N.: Metamathematics, Machines, and Gödel’s Proof. Cambridge University Press, Cambridge (1994)CrossRefMATH

72.

Slind, K.: Reasoning about terminating functional programs. Ph.D. thesis, Technical University of Munich (1999). https://mediatum.ub.tum.de/?id=601660

73.

Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: F. van Raamsdonk (ed.) RTA ’13, LIPIcs, vol. 21, pp. 287–302. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2013)

74.

Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp. 140–145. Springer, New York (2009)

75.

Wenzel, M.: Isar—a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOL’s 1999, LNCS, vol. 1690, pp. 167–183. Springer, New York (1999)

Titel: Formalization of the Resolution Calculus for First-Order Logic
verfasst von: Anders Schlichtkrull
Publikationsdatum: 20.01.2018
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 1-4/2018
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-017-9447-z

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1-4/2018

Introduction to Milestones in Interactive Theorem Proving

The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar

Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

Verified iptables Firewall Analysis and Verification