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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 6/2020

23.09.2019

First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice

verfasst von: Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant

Erschienen in: Journal of Automated Reasoning | Ausgabe 6/2020

Einloggen

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

search-config
loading …

Abstract

We discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with the introduction of a rewrite feature. Deduction modulo theory is an extension of predicate calculus with rewriting both on terms and propositions. It is well suited for proof search in theories because it turns many axioms into rewrite rules. We introduce two automated reasoning systems that have been built to extend other provers with Deduction modulo theory. The first one is Zenon Modulo, a tableau-based tool able to deal with polymorphic first-order logic with equality, while the second one is iProverModulo, a resolution-based system dealing with first-order logic with equality. We also provide some experimental results run on benchmarks that show the beneficial impact of the extension on these two tools and their underlying proof search methods. Finally, we describe the two backends of these systems to the Dedukti universal proof checker, which also relies on Deduction modulo theory, and which allows us to verify the proofs produced by these tools.
Nächster Artikel Efficient Strategies for CEGAR-Based Model Checking

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
This does not strictly conform to Definition 9, as two equivalents terms \(t \equiv u\) must receive the same interpretation. This can be technically fixed by letting D be composed of equivalence classes of terms, or by interpreting terms by their normal forms (it requires confluence and termination), or by dropping the \({\llbracket t \rrbracket }_\varphi = {\llbracket u \rrbracket }_\varphi \) constraint over terms in Definition 9.
 
2
This benchmark is publicly available at: http://​bware.​lri.​fr/​.
 
6
The rewrite systems that we designed to present these theories are given at: http://​www.​ensiie.​fr/​~guillaume.​burel/​empty_​iProverModulo.​html.​en.
 
Literatur
1.
Abrial, J.R.: The B-Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)MATH
2.
Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)MathSciNetMATH
3.
Assaf, A.: A framework for defining computational higher-order logics. Ph.D. Thesis, École polytechnique (2015)
4.
Assaf, A.: Conservativity of embeddings in the \(\lambda \varPi \) calculus modulo rewriting. In: Typed lambda calculi and applications (TLCA), LIPIcs, vol. 38, pp. 31–44. SchlossDagstuhl, Leibniz-Zentrum fuer Informatik, Warsaw (2015)
5.
Assaf, A., Burel, G.: Translating HOL to Dedukti. In: Proof eXchange for theorem proving (PxTP), EPTCS, vol. 186, pp. 74–88. Open Publishing Association, Berlin (2015)
6.
7.
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 19–99. Elsevier, Amsterdam (2001)
8.
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)MathSciNetMATH
9.
Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reason. 28(3), 321–336 (2002)MathSciNetMATH
10.
Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press, Cambridge (2013). ISBN 9780521766142
11.
Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects (FMCO), LNCS, vol. 4111, pp. 364–387. Springer, Amsterdam (2005)
12.
Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)
13.
Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, ThA, Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305–343. Springer, Berlin (2018)
14.
Baumgartner, P.: A Model elimination calculus with built-in theories. In: German Conference on Artificial Intelligence (GWAI), LNCS, vol. 671, pp. 30–42. Springer, Bonn (1992)
15.
Baumgartner, P.: An order theory resolution calculus. In: Logic Programming and Automated Reasoning (LPAR), LNCS, vol. 624, pp. 119–130. Springer, St. Petersburg (1992)
16.
Baumgartner, P., Bax, J., Waldmann, U.: Beagle—a hierarchic superposition theorem prover. In: Conference on Automated Deduction (CADE), LNCS, vol. 9195, pp. 367–377. Springer, Berlin (2015)
17.
Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Conference on Automated Deduction (CADE), LNCS, vol. 7898, pp. 39–57. Springer, Lake Placid (2013)
18.
19.
Beckert, B., Pape, C.: Incremental theory reasoning methods for semantic tableaux. In: Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX), LNCS, vol. 1071, pp. 93–109. Springer, Terrasini (1996)
20.
Beth, E.W.: The Foundations of Mathematics: A Study in the Philosophy of Science. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1959)MATH
21.
Beth, E.W.: Formal Methods: An Introduction to Symbolic Logic and to the Study of Effective Operations in Arithmetic and Logic, Synthese Library, vol. 4. D. Reidel, Dordrecht (1962)MATH
22.
Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. 12(4), 1–52 (2016)MathSciNetMATH
23.
Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Conference on Automated Deduction (CADE), LNCS, vol. 7898. Springer (2013)
24.
Blanqui, F., Jouannaud, J.P., Okada, M.: The calculus of algebraic constructions. In: Rewriting Techniques and Applications (RTA), LNCS, vol. 1631. Springer, Trento (1999)
25.
Bläsius, K.H., Hedtstück, U., Rollinger, C.R. (eds.): Sorts and Types in Artificial Intelligence, Workshop, Eringerfeld, FRG, April 24–26, 1989, Proceedings, LNCS, vol. 418. Springer (1989)
26.
Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: International Workshop on Intermediate Verification Languages (Boogie), Wrocław, Poland, pp. 53–64 (2011)
27.
Boespflug, M., Burel, G.: CoqinE: translating the calculus of inductive constructions into the \(\lambda \varPi \)-calculus modulo. Proof eXchange for Theorem Proving (PxTP), CEUR Workshop Proceedings, vol. 878, pp. 44–50. David Pichardie and Tjark Weber, Manchester (2012)
28.
Boespflug, M., Carbonneaux, Q., Hermant, O.: The \(\lambda \varPi \)-calculus modulo as a universal proof language. In: Proof Exchange for Theorem Proving (PxTP), pp. 28–43. Manchester (2012)
29.
Bonichon, R.: TaMeD: a tableau method for deduction modulo. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 3097, pp. 445–459. Springer, Cork (2004)
30.
Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Logic for Programming. Artificial Intelligence, and Reasoning (LPAR), LNCS/LNAI, vol. 4790, pp. 151–165. Springer, Yerevan (2007)
31.
Bonichon, R., Hermant, O.: A semantic completeness proof for TaMeD. In: Logic for Programming. Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 4246, pp. 167–181. Springer, Phnom Penh (2006)
32.
Bonichon, R., Hermant, O.: On constructive cut admissibility in deduction modulo. In: Types for Proofs and Programs (TYPES), LNCS, vol. 4502, pp. 33–47. Springer, Nottingham (2006)
33.
Boyer, R.S., Moore, J.S.: A theorem prover for a computational logic. In: Conference on Automated Deduction (CADE), vol. 449, pp. 1–15. Springer, Kaiserslautern (1990)
34.
Brauner, P., Houtmann, C., Kirchner, C.: Principles of superdeduction. In: Logic in Computer Science (LICS), pp. 41–50. IEEE Computer Society Press, Wrocław (2007)
35.
Burel, G.: Embedding deduction modulo into a prover. In: Computer Science Logic (CSL), LNCS, vol. 6247, pp. 155–169. Springer, Brno (2010)
36.
Burel, G.: Consistency implies cut admissibility. In: Proof-Search in Axiomatic Theories and Type Theories (PSATTT), Wrocław, Poland (2011)
37.
Burel, G.: Efficiently simulating higher-order arithmetic by a first-order theory modulo. Log. Methods Comput. Sci. 7(1), 1–31 (2011)MathSciNetMATH
38.
Burel, G.: A shallow embedding of resolution and superposition proofs into the \(\lambda \varPi \)-calculus modulo. In: Proof eXchange for Theorem Proving (PxTP), EPiC Series, vol. 14, pp. 43–57. EasyChair (2013)
39.
Burel, G.: Cut admissibility by saturation. In: Rewriting Techniques and Applications (RTA) and Typed Lambda Calculi and Applications (TLCA), LNCS, vol. 8560, pp. 124–138. Springer, Vienna (2014)
40.
Burel, G., Kirchner, C.: Regaining cut admissibility in deduction modulo using abstract completion. Inf. Comput. 208(2), 140–164 (2010)MathSciNetMATH
41.
Bury, G., Cauderlier, R., Halmagrand, P.: Implementing polymorphism in Zenon. in: International Workshop on the Implementation of Logics (IWIL), EPiC Series in Computing, vol. 40, pp. 15–20. EasyChair, Suva (2015)
42.
Bury, G., Cruanes, S., Delahaye, D.: SMT solving modulo tableau and rewriting theories. In: Satisfiability Modulo Theories (SMT). Oxford (2018)
43.
Bury, G., Cruanes, S., Delahaye, D., Euvrard, P.L.: An automation-friendly set theory for the B method. Abstract State Machines, Alloy, B, VDM, and Z (ABZ), LNCS, vol. 10817, pp. 409–414. Springer, Southampton (2018)
44.
Bury, G., Delahaye, D.: Integrating simplex with tableaux. In: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), LNCS, vol. 9323, pp. 86–101. Springer, Wrocław (2015)
45.
Bury, G., Delahaye, D., Doligez, D., Halmagrand, P., Hermant, O.: Automated deduction in the B set theory using typed proof search and deduction modulo. Logic for programming. In: Artificial Intelligence and Reasoning (LPAR), Short Papers, EPiC Series in Computing, vol. 35, pp. 42–58. EasyChair, Suva (2015)
46.
Cauderlier, R.: Object-oriented mechanisms for interoperability between proof systems. Ph.D. Thesis, Conservatoire National des Arts et Métiers (CNAM) (2016)
47.
Cauderlier, R., Dubois, C.: ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Boogie. In: International Colloquium on Theoretical Aspects of Computing (ICTAC), LNCS, vol. 9965, pp. 459–468. Springer, Taipei (2016)
48.
Cauderlier, R., Halmagrand, P.: Checking Zenon Modulo proofs in Boogie. In: Proof eXchange for Theorem Proving (PxTP). EPTCS, vol. 186, pp. 57–73. Open Publishing Association, Berlin (2015)
49.
Chvátal, V.: Linear Programming. Series of Books in the Mathematical Sciences. W. H. Freeman and Company, New York (1983)
50.
51.
Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Typed Lambda Calculi and Applications (TLCA), LNCS, vol. 4583, pp. 102–117. Springer, Paris (2007)
52.
Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)MathSciNetMATH
53.
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)MathSciNetMATH
54.
De Moura, L.M., Bjørner, N.: Efficient E-matching for SMT solvers. In: Conference on Automated Deduction (CADE), LNCS, vol. 4603, pp. 183–198. Springer, Bremen (2007)
55.
Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: when achilles outruns the tortoise using deduction modulo. In: Logic for Programming. Artificial Intelligence, and Reasoning (LPAR), LNCS/ARCoSS, vol. 8312, pp. 274–290. Springer, Stellenbosch (2013)
56.
Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The BWare Project: building a proof platform for the automated verification of B proof obligations. In: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), LNCS, vol. 8477, pp. 126–127. Springer, Toulouse (2014)
57.
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)MathSciNetMATH
58.
Dowek, G.: Confluence as a cut elimination property. In: Rewriting Techniques and Applications (RTA), LNCS, vol. 2706, pp. 2–13. Springer (2003)
59.
Dowek, G.: Polarized resolution modulo. Theoretical computer science (TCS). In: IFIP Advances in Information and Communication Technology, vol. 323, pp. 182–196. Springer, Brisbane (2010)
60.
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. 31(1), 33–72 (2003)MathSciNetMATH
61.
62.
Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Rewriting Techniques and Applications (RTA), LNCS, vol. 3467, pp. 423–437. Springer, Nara (2005)
63.
Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Berlin (1996)MATH
64.
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI), pp. 234–245. ACM, Berlin (2002)
65.
Gaanzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Logic in Computer Science (LICS), pp. 55–64. IEEE Computer Society, Ottawa (2003)
66.
Ganzinger, H., Korovin, K.: Theory instantiation. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 4246, pp. 497–511. Springer, Phnom Penh (2006)
67.
Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Conference on Automated Deduction (CADE), LNCS, vol. 4603, pp. 167–182. Springer, Bremen (2007)
68.
Giese, M.: Incremental closure of free variable tableaux. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 2083, pp. 545–560. Springer, Siena (2001)
69.
Halmagrand, P.: Soundly proving B method formulae using typed sequent calculus. In: International Colloquium on Theoretical Aspects of Computing (ICTAC), LNCS, vol. 9965, pp. 196–213. Springer, Taipei (2016)
70.
Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)MathSciNetMATH
71.
Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Typed Lambda-Calculi and Applications (TLCA), LNCS, vol. 3461, pp. 221–233. Springer, Nara (2005)
72.
73.
Hintikka, J.: Notes on the quantification theory. Societas Scientiarum Fennica, Commentationes Physico-Mathematicae 17(12), 1–13 (1955)MathSciNetMATH
74.
Hintikka, J.: Two papers on symbolic logic: form and content in quantification theory and reductions in the theory of types. Societas Philosophica, Acta philosophica Fennica 8, 7–55 (1955)
75.
Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Tableaux modulo theories using superdeduction: an application to the verification of B proof rules with the Zenon automated theorem prover. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 7364, pp. 332–338. Springer, Manchester (2012)
76.
Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Tableaux modulo theories using superdeduction. Glob. J. Adv. Softw. Eng. 1, 1–13 (2014)MATH
77.
Kifer, M., Wu, J.: A first-order theory of types and polymorphism in logic programming. In: Logic in Computer Science (LICS), pp. 310–321. IEEE Computer Society, Amsterdam (1991)
78.
Korovin, K.: iProver—an instantiation-based theorem prover for first-order logic (system description). In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 5195, pp. 292–298. Springer, Sydney (2008)
79.
Lipton, J., DeMarco, M.: Completeness and cut-elimination in the intuitionistic theory of types. J. Log. Comput. 15, 821–854 (2005)MathSciNetMATH
80.
Maehara, S.: Lattice-valued representation of the cut-elimination theorem. Tsukuba J. Math. 15(2), 509–521 (1991)MathSciNetMATH
81.
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, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131–153. IOS Press, Amsterdam (2009). ISBN 9781586039295
82.
Mentré, D., Marché, C., Filliâtre, J.C., Asuka, M.: Discharging proof obligations from Atelier B using multiple automated provers. In: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), LNCS, vol. 7316, pp. 238–251. Springer, Pisa (2012)
83.
Murray, N.V., Rosenthal, E.: Theory links: applications to automated theorem proving. J. Symb. Comput. 4(2), 173–190 (1987)MathSciNet
84.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)MATH
85.
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)MathSciNetMATH
86.
Nerode, A., Shore, R.A.: Logic for Applications. Texts and Monographs in Computer Science. Springer, Berlin (1993)
87.
Ohlbach, H.J., Siekmann, J.H.: The Markgraf Karl refutation procedure. In: Lassez, J.-L., Plotikin, G. (eds.) Computational Logic, Essays in Honor of Alan Robinson, pp. 41–112. The MIT Press, Cambridge (1991)
88.
Okada, M.: Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic. Theor. Comput. Sci. 227, 333–396 (1999)MathSciNetMATH
89.
Oppacher, F., Suen, E.: HARP: a tableau-based theorem prover. J. Autom. Reason. 4(1), 69–100 (1988)MathSciNet
90.
Petermann, U.: Towards a connection procedure with built in theories. In: Logics in AI, European Workshop JELIA, LNCS, vol. 478, pp. 444–543. Springer, Amsterdam (1990)
91.
Plotkin, G.D.: Building-in equational theories. Mach. Intell. 7, 73–90 (1972)MATH
92.
Prawitz, D.: Natural Deduction. A Proof-Theoretical Study. Studies in Philosophy. Almquist & Wiksell, Stockholm (1965)MATH
93.
Rabe, F.: First-order logic with dependent types. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 4130, pp. 377–391. Springer, Seattle (2006)
94.
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)MathSciNetMATH
95.
Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 5330, pp. 274–289. Springer, Doha (2008)
96.
Saillard, R.: Typechecking in the \(\lambda \varPi \)-calculus modulo: theory and practice. Ph.D. Thesis, École Nationale Supérieure des Mines de Paris (2015)
97.
Schmitt, P.H., Wernecke, W.: Tableau calculus for order sorted logic. In: Sorts and Types in Artificial Intelligence, pp. 49–60. Springer, Berlin (1989)
98.
Schultz, S.: System description: E 0.81. In: International Joint Conference on Automated Reasoning (IJCAR), LNCS, vol. 3097, pp. 223–228. Springer, Cork (2004)
99.
Schwichtenberg, H., Troelstra, A.S.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)MATH
100.
Shankar, N.: Little engines of proof. In: Formal Methods Europe (FME), LNCS, vol. 2391, pp. 1–20. Springer, Copenhagen (2002)
101.
102.
Stickel, M.E.: Automated deduction by theory resolution. J. Autom. Reason. 1(4), 333–355 (1985)MathSciNetMATH
103.
Strub, P.-Y.: Coq modulo theory. In: Computer Science Logic (CSL), LNCS, vol. 6247, pp. 529–543. Springer, Brno (2010)
104.
Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)MATH
105.
Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 7180, pp. 406–419. Springer, Mérida (2012)
106.
Szabo, M.E. (ed.): Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundation of Mathematics. North-Holland, Amsterdam (1969)
107.
108.
Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1–31 (2003)MathSciNetMATH
109.
Walther, C.: Many-sorted inferences in automated theorem proving. In: Sorts and Types in Artificial Intelligence, LNCS, vol. 418, pp. 18–48. Springer, Eringerfeld (1989)
110.
111.
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1965–2013. Elsevier, Amsterdam (2001)
112.
Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12(4), 536–541 (1965)MathSciNetMATH
Metadaten
Titel
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
verfasst von
Guillaume Burel
Guillaume Bury
Raphaël Cauderlier
David Delahaye
Pierre Halmagrand
Olivier Hermant
Publikationsdatum
23.09.2019
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 6/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-019-09533-z

Premium Partner

    Bildnachweise