Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 2/2017

06.08.2016

Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness

verfasst von: Maria Paola Bonacina, David A. Plaisted

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2017

Einloggen

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

search-config
loading …

Abstract

We present a new method for clausal theorem proving, named SGGS from semantically-guided goal-sensitive reasoning. SGGS generalizes to first-order logic the conflict-driven clause learning (CDCL) procedure for propositional satisfiability. Starting from an initial interpretation, used for semantic guidance, SGGS employs a sequence of constrained clauses to represent a candidate model, instance generation to extend it, resolution and other inferences to explain and solve conflicts, amending the model. We prove that SGGS is refutationally complete and model complete in the limit, regardless of initial interpretation. SGGS is also goal sensitive, if the initial interpretation is properly chosen, and proof confluent, because it repairs the current model without undoing steps by backtracking. Thus, SGGS is a complete first-order method that is simultaneously model-based à la CDCL, semantically-guided, goal-sensitive, and proof confluent.
Nächster Artikel A Complete Uniform Substitution Calculus for Differential Dynamic Logic

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
Fußnoten
1
An early forerunner of CDCL was the semantic tree method with lemma generation (cf. pages 284–288 in [53]).
 
Literatur
1.
Alagi, G., Weidenbach, C.: NRCL—a model building approach to the Bernays–Schönfinkel fragment. In: Lutz, C., Ranise, S. (eds.) Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS). Lecture Notes in Artificial Intelligence, vol. 9322, pp. 69–84. Springer, Berlin (2015)CrossRef
2.
Baumgartner, P.: Hyper tableaux—the next generation. In: de Swart, H. (ed.) Proceedings of the 7th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). Lecture Notes in Artificial Intelligence, vol. 1397, pp. 60–76. Springer, Berlin (1998)CrossRef
3.
Baumgartner, P.: FDPLL—a first-order Davis–Putnam–Logeman–Loveland procedure. In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 1831, pp. 200–219. Springer, Berlin (2000)
4.
Baumgartner, P.: Logical engineering with instance-based methods. In: Pfenning, F. (ed.) Proceedings of the 21st International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 4603, pp. 404–409. Springer, Berlin (2007)
5.
Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006)CrossRefMATH
6.
Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: Hermann, M., Voronkov, A. (eds.) Proceedings of the 13th Conference on Logic, Programming and Automated Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol. 4246, pp. 572–586. Springer, Berlin (2006)
7.
Baumgartner, P., Pelzer, B., Tinelli, C.: Model evolution calculus with equality—revised and implemented. J. Symb. Comput. 47(9), 1011–1045 (2012)CrossRefMATH
8.
Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008)MathSciNetCrossRefMATH
9.
Baumgartner, P., Waldmann, U.: Superposition and model evolution combined. In: Schmidt, R. (ed.) Proceedings of the 22nd International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 5663, pp. 17–34. Springer, Berlin (2009)
10.
Bender, M., Pelzer, B., Schon, C.: E-KRHyper 1.4: extensions for unique names and description logic. In: Bonacina, M.P. (ed.) Proceedings of the 24th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 7898, pp. 126–134. Springer, Berlin (2013)
11.
Billon, J.-P.: The disconnection method. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds.) Proceedings of the 5th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). Lecture Notes in Artificial Intelligence, vol. 1071, pp. 110–126. Springer, Berlin (1996)
12.
Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Wooldridge, M.J., Veloso, M. (eds.) Artificial Intelligence Today—Recent Trends and Developments. Lecture Notes in Artificial Intelligence, vol. 1600, pp. 43–84. Springer, Berlin (1999)
13.
14.
Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V.: On first-order model-based reasoning. In: Martí-Oliet, N., Olveczky, P., Talcott, C. (eds.) Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer. Lecture Notes in Computer Science, vol. 9200, pp. 181–204. Springer, Berlin (2015)CrossRef
15.
Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161–189 (2011)MathSciNetCrossRefMATH
16.
Bonacina, M.P., Plaisted, D.A: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of the 28th Workshop on Unification (UNIF). Technical Reports of the Research Institute for Symbolic Computation, pp. 47–54. Johannes Kepler Universität, July (2014). http://​vsl2014.​at/​meetings/​UNIF-index.​html
17.
Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., De Moura, L., Konev, B. (eds.) Proceedings of the 4th Workshop on Practical Aspects in Automated Reasoning (PAAR) (2014). EasyChair Proceedings in Computing (EPiC), vol. 31, pp. 25–38 (2015)
18.
Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reason. 56(2), 113–141 (2016)MathSciNetCrossRefMATH
19.
Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Cambridge (1973)MATH
20.
Chu, H., Plaisted, D.A.: Model finding in semantically guided instance-based theorem proving. Fundam. Inform. 21(3), 221–235 (1994)MathSciNetMATH
21.
Chu, H., Plaisted, D.A.: CLINS-S: a semantically guided first-order theorem prover. J. Autom. Reason. 18(2), 183–188 (1997)CrossRef
22.
Comon, H.: Disunification: a survey. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic—Essays in Honor of Alan Robinson, pp. 322–359. MIT Press, Cambridge (1991)
23.
24.
Davis, M.: The Universal Computer. The Road from Leibniz to Turing. Turing Centenary Edition. Mathematics/Logic/Computing Series. CRC Press, Taylor and Francis Group (2012)
25.
26.
27.
de Moura, L., Bjørner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 5195, pp. 475–490. Springer, Berlin (2008)
28.
Fietzke, A.: Labelled superposition. PhD thesis, Max Planck Institut für Informatik, Saabrücken, October (2013)
29.
Fietzke, A., Weidenbach, C.: Labelled splitting. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 5195, pp. 459–474. Springer, Berlin (2008)
30.
Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 55–64. IEEE Computer Society Press (2003)
31.
Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) Proceedings of the 13th Conference on Logic, Programming and Automated Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol. 4246, pp. 497–511. Springer, Berlin (2006)
32.
Hoder, K., Voronkov, A.: The 481 ways to split a clause and deal with propositional variables. In: Bonacina, M.P. (ed.) Proceedings of the 24th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 7898, pp. 450–464. Springer, Berlin (2013)
33.
Jacobs, S., Waldmann, U.: Comparing instance generation methods for automated reasoning. J. Autom. Reason. 38, 57–78 (2007)MathSciNetCrossRefMATH
34.
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Proceedings of the Conference on Computational Problems in Abstract Algebras, pp. 263–298. Pergamon Press, Oxford (1970)
35.
Korovin, K.: An invitation to instantiation-based reasoning: from theory to practice. In: Schmidt, R. (ed.) Proceedings of the 22nd International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 5663, pp. 163–166. Springer, Berlin (2009)
36.
Korovin, K.: Inst-Gen: a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Artificial Intelligence, vol. 7797, pp. 239–270. Springer, Berlin (2013)CrossRef
37.
Korovin, K., Sticksel, C.: iProver-Eq: an instantiation-based theorem prover with equality. In: Giesl, J., Hähnle, R. (eds.) Proceedings of the 5th International Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 6173, pp. 196–202. Springer, Berlin (2010)
38.
Kovàcs, L., Voronkov, A.: First order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Proceedings of the 25th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 8044, pp. 1–35. Springer, Berlin (2013)
39.
Lee, S.-J., Plaisted, D.A.: Eliminating duplication with the hyperlinking strategy. J. Autom. Reason. 9, 25–42 (1992)CrossRefMATH
40.
Letz, R., Stenz, G.: DCTP—a disconnection calculus theorem prover. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Artificial Intelligence, vol. 2083, pp. 381–385. Springer, Berlin (2001)
41.
Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) Proceedings of the 8th International Conference on Logic, Programming and Automated Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol. 2250, pp. 142–156. Springer, Berlin (2001)
42.
Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Egly, U., Fermüller, C.G. (eds.) Proceedings of the 15th International Conference on Analytic Tableaux and Related Methods (TABLEAUX). Lecture Notes in Artificial Intelligence, vol. 2381, pp. 176–190. Springer, Berlin (2002)
43.
Ludwig, M., Waldmann, U.: An extension of the Knuth–Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) Proceedings of the 14th International Conference on Logic, Programming and Automated Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol. 4790, pp. 348–362. Springer, Berlin (2007)
44.
Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. Technical report, IBM Thomas J. Watson Research Center, Yorktown Heights, NY, USA (1988)
45.
Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proceedings of the 3rd Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 348–457. IEEE Computer Society Press (1988)
46.
Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009)CrossRef
47.
Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) Proceedings of the 9th International Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 310, pp. 415–434. Springer, Berlin (1988)CrossRef
48.
Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 131–153. IOS Press (2009)
49.
Marques Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRef
50.
McCune, W.W.: OTTER 3.0 reference manual and guide. Technical report 94/6, MCS Division, Argonne National Laboratory (1994)
51.
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 39th Design Automation Conference (DAC), pp. 530–535 (2001)
52.
Piskac, R., de Moura, L., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reason. 44(4), 401–424 (2010)MathSciNetCrossRefMATH
53.
Plaisted, D.A.: Mechanical theorem proving. In: Banerji, R.B. (ed.) Formal Techniques in Artificial Intelligence, pp. 269–320. Elsevier, Amsterdam (1990)
54.
Plaisted, D.A., Miller, S.: The relative power of semantics and unification. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Artificial Intelligence, vol. 7797, pp. 317–344. Springer, Berlin (2013)CrossRef
55.
56.
Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) Proceedings of the 25th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 9195, pp. 399–415. Springer, Berlin (2015)
57.
Riazanov, A.: Implementing an efficient theorem prover. PhD thesis, Department of Computer Science, The University of Manchester (July 2003)
58.
Robinson, A.J.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965)MathSciNetMATH
59.
Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) Proceedings of the 19th International Conference on Logic, Programming and Automated Reasoning (LPAR). Lecture Notes in Artificial Intelligence, vol. 8312, pp. 735–743. Springer, Berlin (2013)
60.
61.
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1965–2012. Elsevier, Amsterdam (2001)CrossRef
62.
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R. (ed.) Proceedings of the 22nd International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 5663, pp. 140–145. Springer, Berlin (2009)
63.
Wos, L., Carson, D., Robinson, G.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 536–541 (1965)MathSciNetCrossRefMATH
Metadaten
Titel
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness
verfasst von
Maria Paola Bonacina
David A. Plaisted
Publikationsdatum
06.08.2016
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 2/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9384-2