424:, we know that any consistent theory whose axioms are true for the natural numbers cannot prove all first-order statements true for the natural numbers, even if the list of axioms is allowed to be infinite enumerable. It follows that an automated theorem prover will fail to terminate while searching for a proof precisely when the statement being investigated is undecidable in the theory being used, even if it is true in the model of interest. Despite this theoretical limit, in practice, theorem provers can solve many hard problems, even in models that are not fully described by any first-order theory (such as the
4211:
317:
619:. Generally, automated theorem provers focus on supporting full first-order logic with quantifiers, whereas SMT solvers focus more on supporting various theories (interpreted predicate symbols). ATPs excel at problems with lots of quantifiers, whereas SMT solvers do well on large problems without quantifiers. The line is blurry enough that some ATPs participate in SMT-COMP, while some SMT solvers participate in
759:
598:
theorem proving is one of the most mature subfields of automated theorem proving. The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way. On the other hand, it is still semi-decidable, and a number of sound and complete calculi
475:
There are hybrid theorem proving systems that use model checking as an inference rule. There are also programs that were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the
459:
require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive provers are used for a variety
467:
Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include
274:
The "heuristic" approach of the Logic
Theorist tried to emulate human mathematicians, and could not guarantee that a proof could be found for every valid theorem even in principle. In contrast, other, more systematic algorithms achieved, at least theoretically,
744:
The
Theorem Prover Museum is an initiative to conserve the sources of theorem prover systems for future analysis, since they are important cultural/scientific artefacts. It has the sources of many of the systems mentioned above.
184:
472:, which, in the simplest case, involves brute-force enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force).
480:, which was very controversial as the first claimed mathematical proof that was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are called
730:
Waldmeister is a specialized system for unit-equational first-order logic developed by Arnim Buch and Thomas
Hillenbrand. It won the CASC UEQ division for fourteen consecutive years (1997â2010).
460:
of tasks, but even fully automatic systems have proved a number of interesting and hard theorems, including at least one that has eluded human mathematicians for a long time, namely the
420:. However, for a specific model that may be described by a first-order theory, some statements may be true but undecidable in the theory used to describe the model. For example, by
727:
and KryĆĄtof Hoder. It is now developed by a growing international team. It has won the FOF division (among other divisions) at the CADE ATP System
Competition regularly since 2001.
188:(1931), showing that in any sufficiently strong axiomatic system there are true statements that cannot be proved in the system. This topic was further developed in the 1930s by
1576:
Presburger, MojĆŒesz (1929). "Ăber die VollstĂ€ndigkeit eines gewissen
Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt".
558:
In the late 1960s agencies funding research in automated deduction began to emphasize the need for practical applications. One of the first fruitful areas was that of
1801:
Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer
Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.).
453:
is crucial, and various techniques aiming at making the prover's output smaller, and consequently more easily understandable and checkable, have been developed.
1928:
2089:
ATPs and SMT solvers have complementary strengths. The former handle quantifiers more elegantly, whereas the latter excel on large, mostly ground problems.
2590:
108:, first published 1910â1913, and with a revised second edition in 1927. Russell and Whitehead thought they could derive all mathematical truth using
666:
607:, allow the convenient expression of a wider range of problems than first-order logic, but theorem proving for these logics is less well developed.
442:, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a
3265:
231:
in
Princeton, New Jersey. According to Davis, "Its great triumph was to prove that the sum of two even numbers is even". More ambitious was the
377:
Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the common case of
2125:
In recent years, we have seen a blurring of lines between SMT-COMP and CASC with SMT solvers competing in CASC and ATPs competing in SMT-COMP.
586:
principle. This was the first automated deduction system to demonstrate an ability to solve mathematical problems that were announced in the
3348:
2489:
588:
1645:
1492:
299:. The propositional formulas could then be checked for unsatisfiability using a number of methods. Gilmore's program used conversion to
255:. Also running on a JOHNNIAC, the Logic Theorist constructed proofs from a small set of propositional axioms and three deduction rules:
562:
whereby first-order theorem provers were applied to the problem of verifying the correctness of computer programs in languages such as
338:
874:
737:
636:
516:
and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.
702:
3662:
1602:
3820:
2462:
2328:
2001:
1780:
2608:
3675:
2998:
1908:
1904:
853:
421:
1437:
543:
4235:
3680:
3670:
3407:
3260:
2613:
2304:
2604:
394:
3816:
2445:
2424:
2412:
2376:
2350:
2282:
2258:
364:
3158:
346:
3913:
3657:
2482:
736:
is a first-order logic theorem prover with equality. This is developed by the research group
Automation of Logic,
3218:
2911:
2394:
1387:
547:
2652:
2210:(Technical report). Informatics Research Report. Vol. 2. Division of Informatics, University of Edinburgh.
125:
4174:
3876:
3639:
3634:
3459:
2880:
2564:
1699:
658:
616:
342:
70:, the end of the 19th and early 20th centuries saw the development of modern logic and formalised mathematics.
2202:
2101:
Weber, Tjark; Conchon, Sylvain; DĂ©harbe, David; Heizmann, Matthias; Niemetz, Aina; Reger, Giles (2019-01-01).
4169:
3952:
3869:
3582:
3513:
3390:
2632:
2229:
1337:
991:
563:
90:
4094:
3920:
3606:
3240:
2839:
1598:
1342:
443:
264:
228:
217:
3972:
3967:
3577:
3316:
3245:
2574:
2475:
2390:
2041:." International Joint Conference on Automated Reasoning. Berlin, Germany and Heidelberg: Springer, 2008.
819:
680:
640:
620:
539:
1965:
Luckham, D.; German, S.; von Henke, F.; Karp, R.; Milne, P.; Oppen, D.; Polak, W.; Scherlis, W. (1979).
1670:
Gilmore, Paul (1960). "A proof procedure for quantification theory: its justification and realisation".
643:(CASC), a yearly competition of first-order systems for many important classes of first-order problems.
3901:
3491:
2885:
2853:
2544:
567:
532:
464:. However, these successes are sporadic, and work on hard problems usually requires a proficient user.
570:, etc. Notable among early program verification systems was the Stanford Pascal Verifier developed by
94:, published in 1884, expressed (parts of) mathematics in formal logic. This approach was continued by
4191:
4037:
3535:
3496:
2973:
2618:
1901:
Automatic
Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers
497:
2647:
144:
of a theorem) to be reduced to (potentially infinitely many) propositional satisfiability problems.
4032:
3962:
3501:
3353:
3336:
3059:
2539:
2039:
LEO-II-a cooperative automatic theorem prover for classical higher-order logic (system description)
1811:
1327:
780:
720:
631:
The quality of implemented systems has benefited from the existence of a large library of standard
327:
1966:
4240:
3864:
3841:
3802:
3688:
3629:
3275:
3195:
3039:
2983:
2596:
1432:
843:
809:
449:
Since the proofs generated by automated theorem provers are typically very large, the problem of
331:
300:
133:
2297:
Programming with
Specifications: An Introduction to Anna, A Language for Specifying Ada Programs
1634:
713:. E and SETHEO have been combined (with other systems) in the composite theorem prover E-SETHEO.
4154:
3881:
3859:
3826:
3719:
3565:
3550:
3523:
3474:
3358:
3293:
3118:
3084:
3079:
2953:
2784:
2761:
1806:
1501:
1442:
1149:
1120:
1099:
858:
838:
824:
805:
716:
684:
676:
654:
646:
Some important systems (all have won at least one CASC competition division) are listed below.
99:
1984:
Proceedings of the ACM SIGART international symposium on Methodologies for intelligent systems
4084:
3937:
3729:
3447:
3183:
3089:
2948:
2933:
2814:
2789:
2272:
632:
481:
402:
288:
160:
104:
2248:
870:
148:
4057:
4019:
3896:
3700:
3540:
3464:
3442:
3270:
3228:
3127:
3094:
2958:
2746:
2657:
2038:
1760:
1735:
1402:
1392:
1312:
1297:
1094:
559:
524:
276:
260:
224:
164:
39:
121:
8:
4186:
4077:
4062:
4042:
3999:
3886:
3836:
3762:
3707:
3644:
3437:
3432:
3380:
3148:
3137:
2809:
2709:
2637:
2628:
2624:
2559:
2554:
1407:
1369:
575:
505:
398:
378:
236:
201:
81:
31:
4215:
3984:
3947:
3932:
3925:
3908:
3712:
3694:
3560:
3486:
3469:
3422:
3235:
3144:
2978:
2963:
2923:
2875:
2860:
2848:
2804:
2779:
2549:
2498:
2386:
2268:
2080:
2007:
1947:
1855:
1716:
1543:
604:
583:
579:
477:
461:
438:
152:
67:
47:
35:
3168:
484:). Another example of a program-assisted proof is the one that shows that the game of
4210:
4150:
3957:
3767:
3757:
3649:
3530:
3365:
3341:
3122:
3106:
3011:
2988:
2865:
2834:
2799:
2694:
2529:
2441:
2420:
2408:
2372:
2346:
2324:
2300:
2278:
2254:
2072:
1997:
1847:
1776:
1412:
1397:
1352:
1254:
1017:
814:
706:
595:
520:
450:
390:
296:
129:
2011:
1951:
1720:
578:. This was based on the Stanford Resolution Prover also developed at Stanford using
4164:
4159:
4052:
4009:
3831:
3792:
3787:
3772:
3598:
3555:
3452:
3250:
3200:
2774:
2736:
2318:
2211:
2181:
2114:
2084:
2064:
2025:
1987:
1937:
1859:
1839:
1772:
1768:
1708:
1679:
1453:
1427:
1302:
1065:
650:
501:
386:
280:
248:
172:
168:
141:
95:
51:
43:
405:: given unbounded resources, any valid formula can eventually be proven. However,
397:
states that the theorems (provable statements) are exactly the semantically valid
4145:
4135:
4089:
4072:
4027:
3989:
3891:
3811:
3618:
3545:
3518:
3506:
3412:
3326:
3300:
3255:
3223:
3024:
2826:
2769:
2719:
2684:
2642:
2435:
2368:
1181:
965:
724:
528:
456:
185:
On Formally Undecidable Propositions of Principia Mathematica and Related Systems
156:
85:
76:
2051:
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01).
1900:
4130:
4109:
4067:
4047:
3942:
3797:
3395:
3385:
3375:
3370:
3304:
3178:
3054:
2943:
2938:
2916:
2517:
2431:
1612:
1526:
1475:
1422:
1417:
1131:
1076:
947:
848:
833:
710:
688:
662:
615:
There is substantial overlap between first-order automated theorem provers and
469:
382:
284:
232:
137:
117:
113:
2068:
1843:
1712:
1155:
4229:
4104:
3782:
3289:
3074:
3064:
3034:
3019:
2689:
2292:
2076:
1851:
571:
197:
189:
116:
of formal logic, in principle opening up the process to automation. In 1920,
71:
2052:
1982:
Loveland, D. W. (1986). "Automated theorem proving: Mapping logic into AI".
1827:
179:
4004:
3851:
3752:
3744:
3624:
3572:
3481:
3417:
3400:
3331:
3190:
3049:
2751:
2534:
2314:
1317:
917:
784:
485:
417:
292:
256:
244:
213:
1942:
1923:
4114:
3994:
3173:
3163:
3110:
2794:
2714:
2699:
2579:
2524:
2177:
2159:
1886:
1374:
1259:
1125:
196:, who on the one hand gave two independent but equivalent definitions of
193:
1992:
1873:
653:
is a high-performance prover for full first-order logic, but built on a
3044:
2899:
2870:
2676:
1683:
1307:
1202:
263:, and the replacement of formulas by their definition. The system used
252:
2359:
2119:
2102:
496:
Commercial use of automated theorem proving is mostly concentrated in
4196:
4099:
3152:
3069:
3029:
2993:
2929:
2741:
2731:
2704:
2467:
2404:
2360:
2215:
1876:
Semantics in text processing. step 2008 conference proceedings. 2008.
828:
773:
670:
2320:
Logic for Computer Science: Foundations of Automatic Theorem Proving
316:
4181:
3979:
3427:
3132:
2726:
2400:
1447:
1292:
1287:
903:
769:
279:
for first-order logic. Initial approaches relied on the results of
221:
63:
2277:. Fundamental Studies in Computer Science. Vol. 6. Elsevier.
508:
of modern microprocessors have been designed with extra scrutiny.
287:
to convert a first-order formula into successively larger sets of
267:
guidance, and managed to prove 38 of the first 52 theorems of the
3777:
2569:
1924:"Verification of Array, Record, and Pointer Operations in Pascal"
1332:
938:
692:
425:
216:, the first general-purpose computers became available. In 1954,
2335:
This material may be reproduced for any educational purpose, ...
389:
algorithms are believed to exist for general proof tasks. For a
1986:. Knoxville, Tennessee, United States: ACM Press. p. 224.
1759:
Goel, Shilpi; Ray, Sandip (2022), Chattopadhyay, Anupam (ed.),
1560:
1364:
303:, a form in which the satisfiability of a formula is obvious.
3321:
2667:
2512:
1578:
Comptes Rendus du I CongrÚs de Mathématiciens des Pays Slaves
1347:
1322:
1176:
733:
696:
513:
109:
1887:"Combining Montague semantics and discourse representation."
709:
calculus, originally developed by a team under direction of
2107:
Journal on Satisfiability, Boolean Modeling and Computation
2100:
1041:
912:
657:, originally developed in the automated reasoning group of
1964:
1761:"Microprocessor Assurance and the Role of Theorem Proving"
413:
entailed by a given theory), cannot always be recognized.
2230:"Quantifier elimination in second-order predicate logic."
1828:"Translating Higher-Order Clauses to First-Order Clauses"
1800:
1697:
McCune, W. W. (1997). "Solution of the Robbins Problem".
1273:
1247:
1233:
1228:
1221:
1207:
1195:
1169:
1142:
1113:
1087:
1070:
1058:
1034:
1010:
996:
984:
970:
958:
931:
509:
2139:"The TPTP Problem Library for Automated Theorem Proving"
1525:
Russell, Bertrand; Whitehead, Alfred North (1910â1913).
705:
is a high-performance system based on the goal-directed
626:
2138:
2026:
How to prove higher order theorems in first order logic
1767:, Singapore: Springer Nature Singapore, pp. 1â43,
1635:"Early History and Perspectives of Automated Deduction"
446:
or program, and hence the problem is always decidable.
2050:
1971:(Technical report). Stanford University. CS-TR-79-731.
527:. Automated theorem provers have been integrated with
167:
and gave an algorithm that could determine if a given
16:
Subfield of automated reasoning and mathematical logic
1929:
ACM Transactions on Programming Languages and Systems
1524:
50:
was a major motivating factor for the development of
2247:Chang, Chin-Liang; Lee, Richard Char-Tung (2014) .
1542:Russell, Bertrand; Whitehead, Alfred North (1927).
603:automated systems. More expressive logics, such as
416:The above applies to first-order theories, such as
2365:Automated Reasoning: Introduction and Applications
2363:; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992).
1805:. LNCS. Vol. 3049. Springer. pp. 30â65.
538:Applications of theorem provers are also found in
2204:The automation of proof by mathematical induction
4227:
2385:
1922:Luckham, David C.; Suzuki, Norihisa (Oct 1979).
1899:Luckham, David C.; Suzuki, Norihisa (Mar 1976).
1607:
1541:
2437:First-Order Logic and Automated Theorem Proving
1826:Meng, Jia; Paulson, Lawrence C. (2008-01-01).
667:Baden-WĂŒrttemberg Cooperative State University
553:
306:
2483:
2250:Symbolic Logic and Mechanical Theorem Proving
1921:
1898:
1874:"Wide-coverage semantic analysis with boxer."
1562:Recherches sur la théorie de la démonstration
200:, and on the other gave concrete examples of
178:However, shortly after this positive result,
719:was originally developed and implemented at
589:Notices of the American Mathematical Society
1889:Linguistics and philosophy (1996): 143-186.
1825:
1736:"Computer Math Proof Shows Reasoning Power"
1593:
1591:
1589:
1587:
1548:(2nd ed.). Cambridge University Press.
1531:(1st ed.). Cambridge University Press.
639:(TPTP) Problem Libraryâas well as from the
345:. Unsourced material may be challenged and
2675:
2490:
2476:
2274:Automated Theorem Proving: A Logical Basis
1803:Program Development in Computational Logic
1603:"The Early History of Automated Deduction"
1575:
592:before solutions were formally published.
2228:Gabbay, Dov M., and Hans JĂŒrgen Ohlbach.
2118:
2053:"Extending Sledgehammer with SMT Solvers"
1991:
1941:
1810:
1500:. Breslau: Wilhelm Kobner. Archived from
875:Category:Theorem proving software systems
738:Max Planck Institute for Computer Science
637:Thousands of Problems for Theorem Provers
365:Learn how and when to remove this message
2267:
2246:
1981:
1626:
1584:
1558:
610:
220:programmed Presburger's algorithm for a
207:
2430:
2343:Principles of Automated Theorem Proving
2313:
2291:
1758:
1672:IBM Journal of Research and Development
1669:
1565:(PhD) (in French). University of Paris.
1358:
523:, constructing programs that satisfy a
488:can always be won by the first player.
159:with addition and equality (now called
140:of first-order formulas (and hence the
4228:
2497:
1733:
1696:
519:Other uses of theorem provers include
57:
2471:
2340:
2200:
2136:
1911:from the original on August 12, 2021.
1632:
1597:
1490:
1473:
748:
627:Benchmarks, competitions, and sources
1968:Stanford Pascal verifier user manual
1905:Defense Technical Information Center
752:
343:adding citations to reliable sources
310:
235:in 1956, a deduction system for the
1450:language for formalized mathematics
1438:Program analysis (computer science)
864:
691:. Otter has since been replaced by
436:A simpler, but related, problem is
431:
13:
1734:Kolata, Gina (December 10, 1996).
80:(1879) introduced both a complete
14:
4252:
2456:
1765:Handbook of Computer Architecture
871:Proof assistant § Comparison
546:, where they are used to analyze
128:and, in 1930, to the notion of a
4209:
1903:(Technical Report AD-A027 455).
1281:
757:
315:
291:by instantiating variables with
120:simplified a previous result by
2463:A list of theorem proving tools
2396:Handbook of Automated Reasoning
2222:
2194:
2170:
2152:
2130:
2103:"The SMT Competition 2015â2018"
2094:
2044:
2037:BenzmĂŒller, Christoph, et al. "
2031:
2018:
1975:
1958:
1915:
1892:
1879:
1866:
1819:
1794:
1752:
1727:
1690:
1651:from the original on 2022-10-09
1644:. LNAI (4667). Springer: 2â18.
491:
381:, the problem is decidable but
84:and what is essentially modern
2057:Journal of Automated Reasoning
1832:Journal of Automated Reasoning
1773:10.1007/978-981-15-6401-7_38-1
1700:Journal of Automated Reasoning
1663:
1569:
1552:
1535:
1518:
1484:
1467:
772:format but may read better as
659:Technical University of Munich
599:have been developed, enabling
422:Gödel's incompleteness theorem
391:first-order predicate calculus
62:While the roots of formalised
1:
4170:History of mathematical logic
2239:
1494:Die Grundlagen der Arithmetik
4095:Primitive recursive function
1608:Robinson & Voronkov 2001
1343:SPARK (programming language)
500:and verification. Since the
444:primitive recursive function
401:, so the valid formulas are
395:Gödel's completeness theorem
229:Institute for Advanced Study
7:
2178:"The Theorem Prover Museum"
1388:CurryâHoward correspondence
1380:
820:Method of analytic tableaux
681:Argonne National Laboratory
641:CADE ATP System Competition
554:First-order theorem proving
540:natural language processing
476:machine-aided proof of the
307:Decidability of the problem
46:. Automated reasoning over
10:
4257:
3159:SchröderâBernstein theorem
2886:Monadic predicate calculus
2545:Foundations of mathematics
2440:(2nd ed.). Springer.
1156:TPS Distribution Agreement
1100:Mozilla Public License 1.1
868:
655:purely equational calculus
4236:Automated theorem proving
4205:
4192:Philosophy of mathematics
4141:Automated theorem proving
4123:
4018:
3850:
3743:
3595:
3312:
3288:
3266:Von NeumannâBernaysâGödel
3211:
3105:
3009:
2907:
2898:
2825:
2760:
2666:
2588:
2505:
2069:10.1007/s10817-013-9278-5
1844:10.1007/s10817-007-9085-y
548:discourse representations
498:integrated circuit design
409:formulas (those that are
91:Foundations of Arithmetic
20:Automated theorem proving
2341:Duffy, David A. (1991).
1633:Bibel, Wolfgang (2007).
1460:
854:Higher-order unification
844:Binary decision diagrams
126:LöwenheimâSkolem theorem
3842:Self-verifying theories
3663:Tarski's axiomatization
2614:Tarski's undefinability
2609:incompleteness theorems
2323:(2nd ed.). Dover.
1713:10.1023/A:1005843212881
1491:Frege, Gottlob (1884).
1474:Frege, Gottlob (1879).
1433:Computer algebra system
781:converting this article
695:, which is paired with
661:under the direction of
301:disjunctive normal form
134:Herbrand interpretation
4216:Mathematics portal
3827:Proof of impossibility
3475:propositional variable
2785:Propositional calculus
1480:. Verlag Louis Neuert.
1443:General Problem Solver
1150:Theorem Proving System
859:Quantifier elimination
839:Mathematical induction
806:First-order resolution
685:first-order resolution
289:propositional formulae
82:propositional calculus
4085:Kolmogorov complexity
4038:Computably enumerable
3938:Model complete theory
3730:Principia Mathematica
2790:Propositional formula
2619:BanachâTarski paradox
1943:10.1145/357073.357078
1559:Herbrand, J. (1930).
1545:Principia Mathematica
1528:Principia Mathematica
721:Manchester University
611:Relationship with SMT
482:non-surveyable proofs
403:computably enumerable
261:variable substitution
241:Principia Mathematica
208:First implementations
202:undecidable questions
161:Presburger arithmetic
105:Principia Mathematica
102:in their influential
40:mathematical theorems
38:dealing with proving
4033:ChurchâTuring thesis
4020:Computability theory
3229:continuum hypothesis
2747:Square of opposition
2605:Gödel's completeness
2201:Bundy, Alan (1999).
1403:Computer-aided proof
1393:Symbolic computation
1359:Proprietary software
560:program verification
525:formal specification
506:floating point units
399:well-formed formulas
339:improve this section
225:vacuum-tube computer
4187:Mathematical object
4078:P versus NP problem
4043:Computable function
3837:Reverse mathematics
3763:Logical consequence
3640:primitive recursive
3635:elementary function
3408:Free/bound variable
3261:TarskiâGrothendieck
2780:Logical connectives
2710:Logical equivalence
2560:Logical consequence
2269:Loveland, Donald W.
1993:10.1145/12808.12833
1885:Muskens, Reinhard.
1580:. Warszawa: 92â101.
1408:Formal verification
1370:Wolfram Mathematica
881:
679:, developed at the
605:higher-order logics
576:Stanford University
379:propositional logic
237:propositional logic
175:was true or false.
58:Logical foundations
32:automated reasoning
30:) is a subfield of
28:automated deduction
3985:Transfer principle
3948:Semantics of logic
3933:Categorical theory
3909:Non-standard model
3423:Logical connective
2550:Information theory
2499:Mathematical logic
2137:Sutcliffe, Geoff.
2024:Kerber, Manfred. "
1740:The New York Times
1684:10.1147/rd.41.0028
1059:September 28, 2017
879:
783:, if appropriate.
749:Popular techniques
580:John Alan Robinson
504:, the complicated
478:four color theorem
462:Robbins conjecture
439:proof verification
259:, (propositional)
153:first-order theory
149:MojĆŒesz Presburger
138:(un)satisfiability
48:mathematical proof
36:mathematical logic
4223:
4222:
4155:Abstract category
3958:Theories of truth
3768:Rule of inference
3758:Natural deduction
3739:
3738:
3284:
3283:
2989:Cartesian product
2894:
2893:
2800:Many-valued logic
2775:Boolean functions
2658:Russell's paradox
2633:diagonal argument
2530:First-order logic
2330:978-0-486-78082-5
2164:vprover.github.io
2120:10.3233/SAT190123
2003:978-0-89791-206-8
1782:978-981-15-6401-7
1413:Logic programming
1398:Ramanujan machine
1353:Z3 Theorem Prover
1279:
1278:
1274:November 19, 2019
1255:Z3 Theorem Prover
1143:December 14, 2017
904:YYYY-mm-dd format
815:Model elimination
802:
801:
707:model elimination
521:program synthesis
451:proof compression
385:, and hence only
375:
374:
367:
297:Herbrand universe
163:in his honor) is
130:Herbrand universe
124:, leading to the
122:Leopold Löwenheim
44:computer programs
4248:
4214:
4213:
4165:History of logic
4160:Category of sets
4053:Decision problem
3832:Ordinal analysis
3773:Sequent calculus
3671:Boolean algebras
3611:
3610:
3585:
3556:logical/constant
3310:
3309:
3296:
3219:ZermeloâFraenkel
2970:Set operations:
2905:
2904:
2842:
2673:
2672:
2653:LöwenheimâSkolem
2540:Formal semantics
2492:
2485:
2478:
2469:
2468:
2451:
2418:
2391:Voronkov, Andrei
2382:
2367:(2nd ed.).
2356:
2337:
2315:Gallier, Jean H.
2310:
2288:
2264:
2233:
2226:
2220:
2219:
2209:
2198:
2192:
2191:
2189:
2188:
2182:Michael Kohlhase
2174:
2168:
2167:
2156:
2150:
2149:
2147:
2145:
2134:
2128:
2127:
2122:
2098:
2092:
2091:
2048:
2042:
2035:
2029:
2022:
2016:
2015:
1995:
1979:
1973:
1972:
1962:
1956:
1955:
1945:
1919:
1913:
1912:
1896:
1890:
1883:
1877:
1870:
1864:
1863:
1823:
1817:
1816:
1814:
1798:
1792:
1791:
1790:
1789:
1756:
1750:
1749:
1747:
1746:
1731:
1725:
1724:
1694:
1688:
1687:
1667:
1661:
1660:
1658:
1656:
1650:
1639:
1630:
1624:
1623:
1621:
1620:
1611:. Archived from
1595:
1582:
1581:
1573:
1567:
1566:
1556:
1550:
1549:
1539:
1533:
1532:
1522:
1516:
1515:
1513:
1512:
1506:
1499:
1488:
1482:
1481:
1471:
1454:De Bruijn factor
1428:Proof complexity
1275:
1249:
1248:October 11, 2017
1223:
1197:
1171:
1170:February 4, 2012
1144:
1115:
1089:
1060:
1036:
1012:
1011:January 14, 2013
986:
960:
933:
907:
882:
878:
865:Software systems
797:
794:
788:
779:You can help by
761:
760:
753:
544:formal semantics
529:proof assistants
502:Pentium FDIV bug
457:Proof assistants
432:Related problems
418:Peano arithmetic
387:exponential-time
370:
363:
359:
356:
350:
319:
311:
249:Herbert A. Simon
151:showed that the
52:computer science
4256:
4255:
4251:
4250:
4249:
4247:
4246:
4245:
4226:
4225:
4224:
4219:
4208:
4201:
4146:Category theory
4136:Algebraic logic
4119:
4090:Lambda calculus
4028:Church encoding
4014:
3990:Truth predicate
3846:
3812:Complete theory
3735:
3604:
3600:
3596:
3591:
3583:
3303: and
3299:
3294:
3280:
3256:New Foundations
3224:axiom of choice
3207:
3169:Gödel numbering
3109: and
3101:
3005:
2890:
2840:
2821:
2770:Boolean algebra
2756:
2720:Equiconsistency
2685:Classical logic
2662:
2643:Halting problem
2631: and
2607: and
2595: and
2594:
2589:Theorems (
2584:
2501:
2496:
2459:
2454:
2448:
2432:Fitting, Melvin
2415:
2399:. Vol. I.
2393:, eds. (2001).
2379:
2353:
2331:
2307:
2285:
2261:
2242:
2237:
2236:
2227:
2223:
2207:
2199:
2195:
2186:
2184:
2176:
2175:
2171:
2158:
2157:
2153:
2143:
2141:
2135:
2131:
2099:
2095:
2049:
2045:
2036:
2032:
2023:
2019:
2004:
1980:
1976:
1963:
1959:
1920:
1916:
1897:
1893:
1884:
1880:
1871:
1867:
1824:
1820:
1799:
1795:
1787:
1785:
1783:
1757:
1753:
1744:
1742:
1732:
1728:
1695:
1691:
1668:
1664:
1654:
1652:
1648:
1637:
1631:
1627:
1618:
1616:
1596:
1585:
1574:
1570:
1557:
1553:
1540:
1536:
1523:
1519:
1510:
1508:
1504:
1497:
1489:
1485:
1477:Begriffsschrift
1472:
1468:
1463:
1458:
1383:
1361:
1284:
1182:FreeBSD license
1126:Vampire License
901:
877:
867:
798:
792:
789:
778:
762:
758:
751:
725:Andrei Voronkov
629:
613:
556:
494:
434:
371:
360:
354:
351:
336:
320:
309:
243:, developed by
210:
157:natural numbers
114:inference rules
86:predicate logic
77:Begriffsschrift
60:
22:(also known as
17:
12:
11:
5:
4254:
4244:
4243:
4241:Formal methods
4238:
4221:
4220:
4206:
4203:
4202:
4200:
4199:
4194:
4189:
4184:
4179:
4178:
4177:
4167:
4162:
4157:
4148:
4143:
4138:
4133:
4131:Abstract logic
4127:
4125:
4121:
4120:
4118:
4117:
4112:
4110:Turing machine
4107:
4102:
4097:
4092:
4087:
4082:
4081:
4080:
4075:
4070:
4065:
4060:
4050:
4048:Computable set
4045:
4040:
4035:
4030:
4024:
4022:
4016:
4015:
4013:
4012:
4007:
4002:
3997:
3992:
3987:
3982:
3977:
3976:
3975:
3970:
3965:
3955:
3950:
3945:
3943:Satisfiability
3940:
3935:
3930:
3929:
3928:
3918:
3917:
3916:
3906:
3905:
3904:
3899:
3894:
3889:
3884:
3874:
3873:
3872:
3867:
3860:Interpretation
3856:
3854:
3848:
3847:
3845:
3844:
3839:
3834:
3829:
3824:
3814:
3809:
3808:
3807:
3806:
3805:
3795:
3790:
3780:
3775:
3770:
3765:
3760:
3755:
3749:
3747:
3741:
3740:
3737:
3736:
3734:
3733:
3725:
3724:
3723:
3722:
3717:
3716:
3715:
3710:
3705:
3685:
3684:
3683:
3681:minimal axioms
3678:
3667:
3666:
3665:
3654:
3653:
3652:
3647:
3642:
3637:
3632:
3627:
3614:
3612:
3593:
3592:
3590:
3589:
3588:
3587:
3575:
3570:
3569:
3568:
3563:
3558:
3553:
3543:
3538:
3533:
3528:
3527:
3526:
3521:
3511:
3510:
3509:
3504:
3499:
3494:
3484:
3479:
3478:
3477:
3472:
3467:
3457:
3456:
3455:
3450:
3445:
3440:
3435:
3430:
3420:
3415:
3410:
3405:
3404:
3403:
3398:
3393:
3388:
3378:
3373:
3371:Formation rule
3368:
3363:
3362:
3361:
3356:
3346:
3345:
3344:
3334:
3329:
3324:
3319:
3313:
3307:
3290:Formal systems
3286:
3285:
3282:
3281:
3279:
3278:
3273:
3268:
3263:
3258:
3253:
3248:
3243:
3238:
3233:
3232:
3231:
3226:
3215:
3213:
3209:
3208:
3206:
3205:
3204:
3203:
3193:
3188:
3187:
3186:
3179:Large cardinal
3176:
3171:
3166:
3161:
3156:
3142:
3141:
3140:
3135:
3130:
3115:
3113:
3103:
3102:
3100:
3099:
3098:
3097:
3092:
3087:
3077:
3072:
3067:
3062:
3057:
3052:
3047:
3042:
3037:
3032:
3027:
3022:
3016:
3014:
3007:
3006:
3004:
3003:
3002:
3001:
2996:
2991:
2986:
2981:
2976:
2968:
2967:
2966:
2961:
2951:
2946:
2944:Extensionality
2941:
2939:Ordinal number
2936:
2926:
2921:
2920:
2919:
2908:
2902:
2896:
2895:
2892:
2891:
2889:
2888:
2883:
2878:
2873:
2868:
2863:
2858:
2857:
2856:
2846:
2845:
2844:
2831:
2829:
2823:
2822:
2820:
2819:
2818:
2817:
2812:
2807:
2797:
2792:
2787:
2782:
2777:
2772:
2766:
2764:
2758:
2757:
2755:
2754:
2749:
2744:
2739:
2734:
2729:
2724:
2723:
2722:
2712:
2707:
2702:
2697:
2692:
2687:
2681:
2679:
2670:
2664:
2663:
2661:
2660:
2655:
2650:
2645:
2640:
2635:
2623:Cantor's
2621:
2616:
2611:
2601:
2599:
2586:
2585:
2583:
2582:
2577:
2572:
2567:
2562:
2557:
2552:
2547:
2542:
2537:
2532:
2527:
2522:
2521:
2520:
2509:
2507:
2503:
2502:
2495:
2494:
2487:
2480:
2472:
2466:
2465:
2458:
2457:External links
2455:
2453:
2452:
2446:
2428:
2413:
2387:Robinson, Alan
2383:
2377:
2357:
2351:
2338:
2329:
2311:
2306:978-1461396871
2305:
2293:Luckham, David
2289:
2283:
2265:
2259:
2243:
2241:
2238:
2235:
2234:
2221:
2193:
2169:
2151:
2129:
2113:(1): 221â259.
2093:
2063:(1): 109â128.
2043:
2030:
2017:
2002:
1974:
1957:
1936:(2): 226â244.
1914:
1891:
1878:
1865:
1818:
1812:10.1.1.62.4976
1793:
1781:
1751:
1726:
1707:(3): 263â276.
1689:
1662:
1625:
1583:
1568:
1551:
1534:
1517:
1483:
1465:
1464:
1462:
1459:
1457:
1456:
1451:
1445:
1440:
1435:
1430:
1425:
1423:Model checking
1420:
1418:Proof checking
1415:
1410:
1405:
1400:
1395:
1390:
1384:
1382:
1379:
1378:
1377:
1372:
1367:
1360:
1357:
1356:
1355:
1350:
1345:
1340:
1335:
1330:
1325:
1320:
1315:
1310:
1305:
1300:
1295:
1290:
1283:
1280:
1277:
1276:
1271:
1268:
1265:
1262:
1257:
1251:
1250:
1245:
1242:
1239:
1236:
1231:
1225:
1224:
1219:
1216:
1213:
1210:
1205:
1199:
1198:
1193:
1190:
1187:
1184:
1179:
1173:
1172:
1167:
1164:
1161:
1158:
1153:
1146:
1145:
1140:
1137:
1134:
1132:System on TPTP
1128:
1123:
1117:
1116:
1111:
1108:
1105:
1102:
1097:
1091:
1090:
1085:
1082:
1079:
1077:System on TPTP
1073:
1068:
1062:
1061:
1056:
1053:
1050:
1047:
1044:
1038:
1037:
1032:
1029:
1026:
1023:
1020:
1014:
1013:
1008:
1005:
1002:
999:
994:
988:
987:
982:
979:
976:
973:
968:
962:
961:
956:
953:
950:
948:System on TPTP
944:
941:
935:
934:
929:
926:
923:
920:
915:
909:
908:
898:
895:
892:
889:
886:
866:
863:
862:
861:
856:
851:
846:
841:
836:
834:Model checking
831:
822:
817:
812:
800:
799:
765:
763:
756:
750:
747:
742:
741:
731:
728:
714:
711:Wolfgang Bibel
700:
689:paramodulation
683:, is based on
674:
663:Wolfgang Bibel
628:
625:
612:
609:
555:
552:
493:
490:
470:model checking
433:
430:
383:co-NP-complete
373:
372:
323:
321:
314:
308:
305:
233:Logic Theorist
212:Shortly after
209:
206:
118:Thoralf Skolem
59:
56:
15:
9:
6:
4:
3:
2:
4253:
4242:
4239:
4237:
4234:
4233:
4231:
4218:
4217:
4212:
4204:
4198:
4195:
4193:
4190:
4188:
4185:
4183:
4180:
4176:
4173:
4172:
4171:
4168:
4166:
4163:
4161:
4158:
4156:
4152:
4149:
4147:
4144:
4142:
4139:
4137:
4134:
4132:
4129:
4128:
4126:
4122:
4116:
4113:
4111:
4108:
4106:
4105:Recursive set
4103:
4101:
4098:
4096:
4093:
4091:
4088:
4086:
4083:
4079:
4076:
4074:
4071:
4069:
4066:
4064:
4061:
4059:
4056:
4055:
4054:
4051:
4049:
4046:
4044:
4041:
4039:
4036:
4034:
4031:
4029:
4026:
4025:
4023:
4021:
4017:
4011:
4008:
4006:
4003:
4001:
3998:
3996:
3993:
3991:
3988:
3986:
3983:
3981:
3978:
3974:
3971:
3969:
3966:
3964:
3961:
3960:
3959:
3956:
3954:
3951:
3949:
3946:
3944:
3941:
3939:
3936:
3934:
3931:
3927:
3924:
3923:
3922:
3919:
3915:
3914:of arithmetic
3912:
3911:
3910:
3907:
3903:
3900:
3898:
3895:
3893:
3890:
3888:
3885:
3883:
3880:
3879:
3878:
3875:
3871:
3868:
3866:
3863:
3862:
3861:
3858:
3857:
3855:
3853:
3849:
3843:
3840:
3838:
3835:
3833:
3830:
3828:
3825:
3822:
3821:from ZFC
3818:
3815:
3813:
3810:
3804:
3801:
3800:
3799:
3796:
3794:
3791:
3789:
3786:
3785:
3784:
3781:
3779:
3776:
3774:
3771:
3769:
3766:
3764:
3761:
3759:
3756:
3754:
3751:
3750:
3748:
3746:
3742:
3732:
3731:
3727:
3726:
3721:
3720:non-Euclidean
3718:
3714:
3711:
3709:
3706:
3704:
3703:
3699:
3698:
3696:
3693:
3692:
3690:
3686:
3682:
3679:
3677:
3674:
3673:
3672:
3668:
3664:
3661:
3660:
3659:
3655:
3651:
3648:
3646:
3643:
3641:
3638:
3636:
3633:
3631:
3628:
3626:
3623:
3622:
3620:
3616:
3615:
3613:
3608:
3602:
3597:Example
3594:
3586:
3581:
3580:
3579:
3576:
3574:
3571:
3567:
3564:
3562:
3559:
3557:
3554:
3552:
3549:
3548:
3547:
3544:
3542:
3539:
3537:
3534:
3532:
3529:
3525:
3522:
3520:
3517:
3516:
3515:
3512:
3508:
3505:
3503:
3500:
3498:
3495:
3493:
3490:
3489:
3488:
3485:
3483:
3480:
3476:
3473:
3471:
3468:
3466:
3463:
3462:
3461:
3458:
3454:
3451:
3449:
3446:
3444:
3441:
3439:
3436:
3434:
3431:
3429:
3426:
3425:
3424:
3421:
3419:
3416:
3414:
3411:
3409:
3406:
3402:
3399:
3397:
3394:
3392:
3389:
3387:
3384:
3383:
3382:
3379:
3377:
3374:
3372:
3369:
3367:
3364:
3360:
3357:
3355:
3354:by definition
3352:
3351:
3350:
3347:
3343:
3340:
3339:
3338:
3335:
3333:
3330:
3328:
3325:
3323:
3320:
3318:
3315:
3314:
3311:
3308:
3306:
3302:
3297:
3291:
3287:
3277:
3274:
3272:
3269:
3267:
3264:
3262:
3259:
3257:
3254:
3252:
3249:
3247:
3244:
3242:
3241:KripkeâPlatek
3239:
3237:
3234:
3230:
3227:
3225:
3222:
3221:
3220:
3217:
3216:
3214:
3210:
3202:
3199:
3198:
3197:
3194:
3192:
3189:
3185:
3182:
3181:
3180:
3177:
3175:
3172:
3170:
3167:
3165:
3162:
3160:
3157:
3154:
3150:
3146:
3143:
3139:
3136:
3134:
3131:
3129:
3126:
3125:
3124:
3120:
3117:
3116:
3114:
3112:
3108:
3104:
3096:
3093:
3091:
3088:
3086:
3085:constructible
3083:
3082:
3081:
3078:
3076:
3073:
3071:
3068:
3066:
3063:
3061:
3058:
3056:
3053:
3051:
3048:
3046:
3043:
3041:
3038:
3036:
3033:
3031:
3028:
3026:
3023:
3021:
3018:
3017:
3015:
3013:
3008:
3000:
2997:
2995:
2992:
2990:
2987:
2985:
2982:
2980:
2977:
2975:
2972:
2971:
2969:
2965:
2962:
2960:
2957:
2956:
2955:
2952:
2950:
2947:
2945:
2942:
2940:
2937:
2935:
2931:
2927:
2925:
2922:
2918:
2915:
2914:
2913:
2910:
2909:
2906:
2903:
2901:
2897:
2887:
2884:
2882:
2879:
2877:
2874:
2872:
2869:
2867:
2864:
2862:
2859:
2855:
2852:
2851:
2850:
2847:
2843:
2838:
2837:
2836:
2833:
2832:
2830:
2828:
2824:
2816:
2813:
2811:
2808:
2806:
2803:
2802:
2801:
2798:
2796:
2793:
2791:
2788:
2786:
2783:
2781:
2778:
2776:
2773:
2771:
2768:
2767:
2765:
2763:
2762:Propositional
2759:
2753:
2750:
2748:
2745:
2743:
2740:
2738:
2735:
2733:
2730:
2728:
2725:
2721:
2718:
2717:
2716:
2713:
2711:
2708:
2706:
2703:
2701:
2698:
2696:
2693:
2691:
2690:Logical truth
2688:
2686:
2683:
2682:
2680:
2678:
2674:
2671:
2669:
2665:
2659:
2656:
2654:
2651:
2649:
2646:
2644:
2641:
2639:
2636:
2634:
2630:
2626:
2622:
2620:
2617:
2615:
2612:
2610:
2606:
2603:
2602:
2600:
2598:
2592:
2587:
2581:
2578:
2576:
2573:
2571:
2568:
2566:
2563:
2561:
2558:
2556:
2553:
2551:
2548:
2546:
2543:
2541:
2538:
2536:
2533:
2531:
2528:
2526:
2523:
2519:
2516:
2515:
2514:
2511:
2510:
2508:
2504:
2500:
2493:
2488:
2486:
2481:
2479:
2474:
2473:
2470:
2464:
2461:
2460:
2449:
2447:9781461223603
2443:
2439:
2438:
2433:
2429:
2426:
2425:9780262182232
2422:
2416:
2414:9780080532790
2410:
2406:
2402:
2398:
2397:
2392:
2388:
2384:
2380:
2378:9780079112514
2374:
2370:
2366:
2362:
2358:
2354:
2352:9780471927846
2348:
2344:
2339:
2336:
2332:
2326:
2322:
2321:
2316:
2312:
2308:
2302:
2298:
2294:
2290:
2286:
2284:9781483296777
2280:
2276:
2275:
2270:
2266:
2262:
2260:9780080917283
2256:
2252:
2251:
2245:
2244:
2231:
2225:
2217:
2213:
2206:
2205:
2197:
2183:
2179:
2173:
2165:
2161:
2155:
2140:
2133:
2126:
2121:
2116:
2112:
2108:
2104:
2097:
2090:
2086:
2082:
2078:
2074:
2070:
2066:
2062:
2058:
2054:
2047:
2040:
2034:
2027:
2021:
2013:
2009:
2005:
1999:
1994:
1989:
1985:
1978:
1970:
1969:
1961:
1953:
1949:
1944:
1939:
1935:
1931:
1930:
1925:
1918:
1910:
1906:
1902:
1895:
1888:
1882:
1875:
1869:
1861:
1857:
1853:
1849:
1845:
1841:
1837:
1833:
1829:
1822:
1813:
1808:
1804:
1797:
1784:
1778:
1774:
1770:
1766:
1762:
1755:
1741:
1737:
1730:
1722:
1718:
1714:
1710:
1706:
1702:
1701:
1693:
1685:
1681:
1677:
1673:
1666:
1647:
1643:
1636:
1629:
1615:on 2012-07-28
1614:
1610:
1609:
1604:
1600:
1599:Davis, Martin
1594:
1592:
1590:
1588:
1579:
1572:
1564:
1563:
1555:
1547:
1546:
1538:
1530:
1529:
1521:
1507:on 2007-09-26
1503:
1496:
1495:
1487:
1479:
1478:
1470:
1466:
1455:
1452:
1449:
1446:
1444:
1441:
1439:
1436:
1434:
1431:
1429:
1426:
1424:
1421:
1419:
1416:
1414:
1411:
1409:
1406:
1404:
1401:
1399:
1396:
1394:
1391:
1389:
1386:
1385:
1376:
1373:
1371:
1368:
1366:
1363:
1362:
1354:
1351:
1349:
1346:
1344:
1341:
1339:
1336:
1334:
1331:
1329:
1326:
1324:
1321:
1319:
1316:
1314:
1311:
1309:
1306:
1304:
1301:
1299:
1296:
1294:
1291:
1289:
1286:
1285:
1282:Free software
1272:
1269:
1266:
1263:
1261:
1258:
1256:
1253:
1252:
1246:
1243:
1240:
1237:
1235:
1232:
1230:
1227:
1226:
1220:
1217:
1214:
1211:
1209:
1206:
1204:
1201:
1200:
1196:November 2005
1194:
1191:
1188:
1185:
1183:
1180:
1178:
1175:
1174:
1168:
1165:
1162:
1159:
1157:
1154:
1151:
1148:
1147:
1141:
1138:
1135:
1133:
1129:
1127:
1124:
1122:
1119:
1118:
1112:
1109:
1106:
1103:
1101:
1098:
1096:
1093:
1092:
1086:
1083:
1080:
1078:
1074:
1072:
1069:
1067:
1064:
1063:
1057:
1054:
1051:
1048:
1045:
1043:
1040:
1039:
1033:
1030:
1027:
1024:
1021:
1019:
1016:
1015:
1009:
1006:
1003:
1000:
998:
995:
993:
990:
989:
983:
980:
977:
974:
972:
969:
967:
964:
963:
957:
954:
951:
949:
945:
943:Public Domain
942:
940:
939:Prover9/Otter
937:
936:
930:
927:
924:
921:
919:
916:
914:
911:
910:
905:
899:
896:
893:
890:
887:
884:
883:
876:
872:
860:
857:
855:
852:
850:
847:
845:
842:
840:
837:
835:
832:
830:
826:
825:Superposition
823:
821:
818:
816:
813:
811:
807:
804:
803:
796:
793:December 2023
787:is available.
786:
782:
776:
775:
771:
766:This article
764:
755:
754:
746:
739:
735:
732:
729:
726:
722:
718:
715:
712:
708:
704:
701:
698:
694:
690:
686:
682:
678:
675:
672:
668:
665:, and now at
664:
660:
656:
652:
649:
648:
647:
644:
642:
638:
635:examplesâthe
634:
624:
622:
618:
608:
606:
602:
597:
593:
591:
590:
585:
581:
577:
573:
572:David Luckham
569:
565:
561:
551:
549:
545:
541:
536:
534:
530:
526:
522:
517:
515:
511:
507:
503:
499:
489:
487:
483:
479:
473:
471:
465:
463:
458:
454:
452:
447:
445:
441:
440:
429:
427:
423:
419:
414:
412:
408:
404:
400:
396:
392:
388:
384:
380:
369:
366:
358:
348:
344:
340:
334:
333:
329:
324:This section
322:
318:
313:
312:
304:
302:
298:
294:
290:
286:
282:
278:
272:
270:
266:
262:
258:
254:
250:
246:
242:
238:
234:
230:
226:
223:
219:
215:
205:
203:
199:
198:computability
195:
191:
190:Alonzo Church
187:
186:
181:
176:
174:
170:
166:
162:
158:
154:
150:
145:
143:
139:
136:that allowed
135:
131:
127:
123:
119:
115:
111:
107:
106:
101:
97:
93:
92:
87:
83:
79:
78:
73:
69:
65:
55:
53:
49:
45:
41:
37:
33:
29:
25:
21:
4207:
4140:
4005:Ultraproduct
3852:Model theory
3817:Independence
3753:Formal proof
3745:Proof theory
3728:
3701:
3658:real numbers
3630:second-order
3541:Substitution
3418:Metalanguage
3359:conservative
3332:Axiom schema
3276:Constructive
3246:MorseâKelley
3212:Set theories
3191:Aleph number
3184:inaccessible
3090:Grothendieck
2974:intersection
2861:Higher-order
2849:Second-order
2795:Truth tables
2752:Venn diagram
2535:Formal proof
2436:
2395:
2364:
2342:
2334:
2319:
2299:. Springer.
2296:
2273:
2253:. Elsevier.
2249:
2224:
2203:
2196:
2185:. Retrieved
2172:
2163:
2154:
2142:. Retrieved
2132:
2124:
2110:
2106:
2096:
2088:
2060:
2056:
2046:
2033:
2020:
1983:
1977:
1967:
1960:
1933:
1927:
1917:
1894:
1881:
1872:Bos, Johan.
1868:
1838:(1): 35â60.
1835:
1831:
1821:
1802:
1796:
1786:, retrieved
1764:
1754:
1743:. Retrieved
1739:
1729:
1704:
1698:
1692:
1675:
1671:
1665:
1653:. Retrieved
1641:
1628:
1617:. Retrieved
1613:the original
1606:
1577:
1571:
1561:
1554:
1544:
1537:
1527:
1520:
1509:. Retrieved
1502:the original
1493:
1486:
1476:
1469:
1088:July 4, 2017
985:May 15, 2015
918:3-clause BSD
900:Last update
888:License type
790:
785:Editing help
767:
743:
645:
630:
614:
600:
594:
587:
557:
537:
533:Isabelle/HOL
531:, including
518:
495:
492:Applications
486:Connect Four
474:
466:
455:
448:
437:
435:
415:
410:
406:
376:
361:
352:
337:Please help
325:
277:completeness
273:
268:
257:modus ponens
245:Allen Newell
240:
218:Martin Davis
214:World War II
211:
183:
177:
146:
103:
89:
75:
61:
27:
23:
19:
18:
4115:Type theory
4063:undecidable
3995:Truth value
3882:equivalence
3561:non-logical
3174:Enumeration
3164:Isomorphism
3111:cardinality
3095:Von Neumann
3060:Ultrafilter
3025:Uncountable
2959:equivalence
2876:Quantifiers
2866:Fixed-point
2835:First-order
2715:Consistency
2700:Proposition
2677:Traditional
2648:Lindström's
2638:Compactness
2580:Type theory
2525:Cardinality
2369:McGrawâHill
1655:2 September
1375:ResearchCyc
1260:MIT License
891:Web service
880:Comparison
810:unification
617:SMT solvers
596:First-order
194:Alan Turing
66:go back to
4230:Categories
3926:elementary
3619:arithmetic
3487:Quantifier
3465:functional
3337:Expression
3055:Transitive
2999:identities
2984:complement
2917:hereditary
2900:Set theory
2361:Wos, Larry
2240:References
2187:2022-11-20
2028:." (1999).
1788:2024-02-10
1745:2008-10-11
1619:2012-09-08
1511:2012-09-02
1308:IsaPlanner
1203:IsaPlanner
897:Standalone
869:See also:
584:resolution
355:April 2010
253:J. C. Shaw
182:published
180:Kurt Gödel
4197:Supertask
4100:Recursion
4058:decidable
3892:saturated
3870:of models
3793:deductive
3788:axiomatic
3708:Hilbert's
3695:Euclidean
3676:canonical
3599:axiomatic
3531:Signature
3460:Predicate
3349:Extension
3271:Ackermann
3196:Operation
3075:Universal
3065:Recursive
3040:Singleton
3035:Inhabited
3020:Countable
3010:Types of
2994:power set
2964:partition
2881:Predicate
2827:Predicate
2742:Syllogism
2732:Soundness
2705:Inference
2695:Tautology
2597:paradoxes
2434:(2012) .
2405:MIT Press
2345:. Wiley.
2317:(2015) .
2271:(2016) .
2216:1842/3394
2160:"History"
2077:1573-0670
1852:1573-0670
1807:CiteSeerX
1678:: 28â35.
829:rewriting
827:and term
671:Stuttgart
633:benchmark
326:does not
295:from the
269:Principia
265:heuristic
165:decidable
147:In 1929,
100:Whitehead
68:Aristotle
4182:Logicism
4175:timeline
4151:Concrete
4010:Validity
3980:T-schema
3973:Kripke's
3968:Tarski's
3963:semantic
3953:Strength
3902:submodel
3897:spectrum
3865:function
3713:Tarski's
3702:Elements
3689:geometry
3645:Robinson
3566:variable
3551:function
3524:spectrum
3514:Sentence
3470:variable
3413:Language
3366:Relation
3327:Automata
3317:Alphabet
3301:language
3155:-jection
3133:codomain
3119:Function
3080:Universe
3050:Infinite
2954:Relation
2737:Validity
2727:Argument
2625:theorem,
2401:Elsevier
2295:(1990).
2012:14361631
1952:10088183
1909:Archived
1721:30847540
1646:Archived
1601:(2001).
1448:Metamath
1381:See also
1293:Automath
1288:Alt-Ergo
1035:May 2009
932:May 2019
426:integers
281:Herbrand
222:JOHNNIAC
173:language
169:sentence
142:validity
4124:Related
3921:Diagram
3819: (
3798:Hilbert
3783:Systems
3778:Theorem
3656:of the
3601:systems
3381:Formula
3376:Grammar
3292: (
3236:General
2949:Forcing
2934:Element
2854:Monadic
2629:paradox
2570:Theorem
2506:General
2232:(1992).
2144:15 July
2085:5389933
1860:7716709
1642:Ki 2007
1333:Prover9
1328:Paradox
1121:Vampire
894:Library
717:Vampire
693:Prover9
407:invalid
347:removed
332:sources
239:of the
227:at the
171:in the
155:of the
96:Russell
3887:finite
3650:Skolem
3603:
3578:Theory
3546:Symbol
3536:String
3519:atomic
3396:ground
3391:closed
3386:atomic
3342:ground
3305:syntax
3201:binary
3128:domain
3045:Finite
2810:finite
2668:Logics
2627:
2575:Theory
2444:
2423:
2411:
2375:
2349:
2327:
2303:
2281:
2257:
2083:
2075:
2010:
2000:
1950:
1858:
1850:
1809:
1779:
1719:
1365:CARINE
873:, and
768:is in
703:SETHEO
564:Pascal
285:Skolem
132:and a
110:axioms
88:. His
3877:Model
3625:Peano
3482:Proof
3322:Arity
3251:Naive
3138:image
3070:Fuzzy
3030:Empty
2979:union
2924:Class
2565:Model
2555:Lemma
2513:Axiom
2208:(PDF)
2081:S2CID
2008:S2CID
1948:S2CID
1856:S2CID
1717:S2CID
1649:(PDF)
1638:(PDF)
1505:(PDF)
1498:(PDF)
1461:Notes
1348:Twelf
1323:NuPRL
1318:Mizar
1177:SPASS
1152:(TPS)
1095:SNARK
997:GPLv2
971:GPLv2
808:with
774:prose
734:SPASS
697:Mace4
677:Otter
601:fully
514:Intel
293:terms
72:Frege
64:logic
4000:Type
3803:list
3607:list
3584:list
3573:Term
3507:rank
3401:open
3295:list
3107:Maps
3012:sets
2871:Free
2841:list
2591:list
2518:list
2442:ISBN
2421:ISBN
2409:ISBN
2373:ISBN
2347:ISBN
2325:ISBN
2301:ISBN
2279:ISBN
2255:ISBN
2146:2019
2073:ISSN
1998:ISBN
1848:ISSN
1777:ISBN
1657:2012
1222:2007
1130:Via
1114:2012
1075:Via
1042:PhoX
966:Jape
959:2009
946:Via
913:ACL2
885:Name
849:DPLL
770:list
687:and
621:CASC
542:and
330:any
328:cite
283:and
251:and
192:and
112:and
98:and
34:and
3687:of
3669:of
3617:of
3149:Sur
3123:Map
2930:Ur-
2912:Set
2419:II
2212:hdl
2115:doi
2065:doi
1988:doi
1938:doi
1840:doi
1769:doi
1709:doi
1680:doi
1338:PVS
1313:LCF
1298:CVC
1270:Yes
1267:Yes
1264:Yes
1244:Yes
1241:Yes
1238:Yes
1234:GPL
1229:KeY
1218:Yes
1215:Yes
1208:GPL
1192:Yes
1189:Yes
1186:Yes
1163:Yes
1139:Yes
1136:Yes
1107:Yes
1084:Yes
1071:GPL
1052:Yes
1028:Yes
1018:EQP
1004:Yes
992:PVS
978:Yes
975:Yes
952:Yes
928:Yes
723:by
669:in
582:'s
574:at
568:Ada
510:AMD
428:).
411:not
341:by
74:'s
42:by
26:or
24:ATP
4232::
4073:NP
3697::
3691::
3621::
3298:),
3153:Bi
3145:In
2407:.
2403:,
2389:;
2371:.
2333:.
2180:.
2162:.
2123:.
2111:11
2109:.
2105:.
2087:.
2079:.
2071:.
2061:51
2059:.
2055:.
2006:.
1996:.
1946:.
1932:.
1926:.
1907:.
1854:.
1846:.
1836:40
1834:.
1830:.
1775:,
1763:,
1738:.
1715:.
1705:19
1703:.
1674:.
1640:.
1605:.
1586:^
1212:No
1166:No
1160:No
1110:No
1104:No
1081:No
1055:No
1049:No
1031:No
1025:No
1007:No
1001:No
981:No
955:No
925:No
922:No
623:.
566:,
550:.
535:.
512:,
393:,
271:.
247:,
204:.
54:.
4153:/
4068:P
3823:)
3609:)
3605:(
3502:â
3497:!
3492:â
3453:=
3448:â
3443:â
3438:â§
3433:âš
3428:ÂŹ
3151:/
3147:/
3121:/
2932:)
2928:(
2815:â
2805:3
2593:)
2491:e
2484:t
2477:v
2450:.
2427:.
2417:.
2381:.
2355:.
2309:.
2287:.
2263:.
2218:.
2214::
2190:.
2166:.
2148:.
2117::
2067::
2014:.
1990::
1954:.
1940::
1934:1
1862:.
1842::
1815:.
1771::
1748:.
1723:.
1711::
1686:.
1682::
1676:4
1659:.
1622:.
1514:.
1303:E
1066:E
1046:?
1022:?
906:)
902:(
795:)
791:(
777:.
740:.
699:.
673:.
651:E
368:)
362:(
357:)
353:(
349:.
335:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.