Reasoning is the ability to make inferences, and automated reasoningis concerned with the building of computing systems that automate thisprocess. Although the overall goal is to mechanize different forms ofreasoning, the term has largely been identified with valid deductivereasoning as practiced in mathematics and formal logic. In thisrespect, automated reasoning is akin to mechanical theorem proving.Building an automated reasoning program means providing an algorithmicdescription to a formal calculus so that it can be implemented on acomputer to prove theorems of the calculus in an efficient manner.Important aspects of this exercise involve defining the class ofproblems the program will be required to solve, deciding what languagewill be used by the program to represent the information given to itas well as new information inferred by the program, specifying themechanism that the program will use to conduct deductive inferences,and figuring out how to perform all these computations efficiently.While basic research work continues in order to provide the necessarytheoretical framework, the field has reached a point where automatedreasoning programs are being used by researchers to attack openquestions in mathematics and logic, provide important applications incomputing science, solve problems in engineering, and find novelapproaches to questions in exact philosophy.

• 1. Introduction
  • 1.1 Problem Domain
  • 1.2 Language Representation
• 2. Deduction Calculi
  • 2.1 Resolution
  • 2.2 Sequent Deduction
  • 2.3 Natural Deduction
  • 2.4 The Matrix Connection Method
  • 2.5 Term Rewriting
  • 2.6 Mathematical Induction
• 3. Other Logics
  • 3.1 Higher-Order Logic
  • 3.2 Non-classical Logics
• 4. Applications
  • 4.1 Logic Programming
  • 4.2 SAT Solvers
  • 4.3 Deductive Computer Algebra
  • 4.4 Formal Verification of Hardware
  • 4.5 Formal Verification of Software
  • 4.6 Logic and Philosophy
  • 4.7 Mathematics
  • 4.8 Artificial Intelligence
• 5. Conclusion
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Introduction

A problem being presented to an automated reasoning program consistsof two main items, namely a statement expressing the particularquestion being asked called theproblem’sconclusion, and a collection of statements expressing all therelevant information available to the program—theproblem’s assumptions. Solving a problem meansproving the conclusion from the given assumptions by the systematicapplication of rules of deduction embedded within the reasoningprogram. The problem solving process ends when one such proof isfound, when the program is able to detect the non-existence of aproof, or when it simply runs out of resources.

1.1 Problem Domain

A first important consideration in the design of an automatedreasoning program is to delineate the class of problems that theprogram will be required to solve—theproblemdomain. The domain can be very large, as would be the casefor a general-purpose theorem prover for first-order logic, or be morerestricted in scope as in a special-purpose theorem prover forTarski’s geometry, or the modal logic K. A typical approach inthe design of an automated reasoning program is to provide it firstwith sufficient logical power (e.g., first-order logic) and thenfurther demarcate its scope to the particular domain of interestdefined by a set ofdomain axioms. To illustrate,EQP, a theorem-proving program for equational logic, was used to solvean open question in Robbins algebra (McCune 1997):Are all Robbinsalgebras Boolean? For this, the program was provided with theaxioms defining a Robbins algebra:

The program was then used to show that a characterization of Booleanalgebra that uses Huntington’s equation, \[-(-x + y) + -(-x + -y) = x,\] followsfrom the axioms. We should remark that this problem is non-trivialsince deciding whether a finite set of equations provides a basis forBoolean algebra is undecidable, that is, it does not permit analgorithmic representation; also, the problem was attacked by Robbins,Huntington, Tarski and many of his students with no success. The keystep was to establish that all Robbins algebras satisfy \[\exists x\exists y(x + y = x),\]since it was known that this formula is a sufficient condition for aRobbins algebra to be Boolean. When EQP was supplied with this pieceof information, the program provided invaluable assistance bycompleting the proof automatically.

A special-purpose theorem prover does not draw its main benefit byrestricting its attention to the domain axioms but from the fact thatthe domain may enjoy particular theorem-proving techniques which canbe hardwired—coded—within the reasoning program itself andwhich may result in a more efficient logic implementation. Much ofEQP’s success at settling the Robbins question can be attributedto its built-in associative-commutative inference mechanisms.

1.2 Language Representation

A second important consideration in the building of an automatedreasoning program is to decide (1) how problems in its domain will bepresented to the reasoning program; (2) how they will actually berepresented internally within the program; and, (3) how the solutionsfound—completed proofs—will be displayed back to the user.There are several formalisms available for this, and the choice isdependent on the problem domain and the underlying deduction calculusused by the reasoning program. The most commonly used formalismsinclude standard first-order logic, typed \(\lambda\)-calculus, andclausal logic. We take up clausal logic here and assume that thereader is familiar with the rudiments of first-order logic; for thetyped \(\lambda\)-calculus the reader may want to check Church 1940.Clausal logic is a quantifier-free variation of first-order logic andhas been the most widely used notation within the automated reasoningcommunity. Some definitions are in order: Aterm is aconstant, a variable, or a function whose arguments are themselvesterms. For example, \(a, x, f(x)\), and \(h(c,f(z),y)\) are all terms.Aliteral is either an atomic formula, e.g. \(F(x)\),or the negation of an atomic formula, e.g. \({\sim}R(x,f(a))\). Twoliterals arecomplementary if one is the negation ofthe other. Aclause is a (possibly empty) finitedisjunction of literals \(l_1\vee \ldots \vee l_n\) where no literalappears more than once in the clause (that is, clauses can bealternatively treated as sets of literals).Groundterms, ground literals, and ground clauses have no variables. Theempty clause, [ ], is the clause having noliterals and, hence, is unsatisfiable—false under anyinterpretation. Some examples: \({\sim}R(a,b)\), and \(F(a)\vee{\sim}R(f(x),b) \vee F(z)\) are both examples of clauses but onlythe former is ground. The general idea is to be able to express aproblem’s formulation as a set of clauses or, equivalently, as aformula inconjunctive normal form (CNF), that is, asa conjunction of clauses.

For formulas already expressed in standard logic notation, there is asystematic two-step procedure for transforming them into conjunctivenormal form. The first step consists in re-expressing a formula into asemantically equivalent formula inprenex normalform, \((\Theta x_1)\ldots(\Theta x_n)\alpha(x_1 ,\ldots,x_n)\), consisting of a string of quantifiers \((\Thetax_1)\ldots(\Theta x_n)\) followed by a quantifier-free expression\(\alpha(x_1 ,\ldots ,x_n)\) called thematrix. Thesecond step in the transformation first converts the matrix intoconjunctive normal form by using well-known logical equivalences suchas DeMorgan’s laws, distribution, double-negation, and others;then, the quantifiers in front of the matrix, which is now inconjunctive normal form, are dropped according to certain rules. Inthe presence of existential quantifiers, this latter step does notalways preserve equivalence and requires the introduction ofSkolem functions whose role is to“simulate” the behaviour of existentially quantifiedvariables. For example, applying the skolemizing process to theformula \[\forall x\exists y\forall z\exists u\forall v[R(x,y,v)\vee{\sim}K(x,z,u,v)]\] requires the introduction of a one-place andtwo-place Skolem functions, \(f\) and \(g\) respectively, resulting inthe formula \[\forall x\forall z\forall v[R(x,f(x),v)\vee{\sim}K(x,z,g(x,z),v)]\] The universal quantifiers can then be removedto obtain the final clause, \(R(x,f(x),v) \vee{\sim}K(x,z,g(x,z),v)\)in our example. The Skolemizing process may not preserve equivalencebut maintains satisfiability, which is enough for clause-basedautomated reasoning.

Although clausal form provides a more uniform and economicalnotation—there are no quantifiers and all formulas aredisjunctions—it has certain disadvantages. One drawback is theincrease in the size of the resulting formula when transformed fromstandard logic notation into clausal form. The increase in size isaccompanied by an increase in cognitive complexity that makes itharder for humans to read proofs written with clauses. Anotherdisadvantage is that the syntactic structure of a formula in standardlogic notation can be used to guide the construction of a proof butthis information is completely lost in the transformation into clausalform.

2. Deduction Calculi

A third important consideration in the building of an automatedreasoning program is the selection of the actual deduction calculusthat will be used by the program to perform its inferences. Asindicated before, the choice is highly dependent on the nature of theproblem domain and there is a fair range of options available:General-purpose theorem proving and problem solving (first-orderlogic, simple type theory), program verification (first-order logic),distributed and concurrent systems (modal and temporal logics),program specification (intuitionistic logic), hardware verification(higher-order logic), logic programming (Horn logic), constraintsatisfaction (propositional clausal logic), mathematics (higher-orderlogic), computational metaphysics (higher-order modal logic), andothers.

A deduction calculus consists of a set of logical axioms and acollection of deduction rules for deriving new formulas frompreviously derived formulas. Solving a problem in the program’sproblem domain then really means establishing a particular formula\(\alpha\)—the problem’s conclusion—from theextended set \(\Gamma\) consisting of the logical axioms, the domainaxioms, and the problem assumptions. That is, the program needs todetermine if \(\Gamma\) entails \(\alpha , \Gamma \vDash \alpha\). Howthe program goes about establishing this semantic fact depends, ofcourse, on the calculus it implements. Some programs may take a verydirect route and attempt to establish that \(\Gamma\vDash \alpha\) by actually constructing a step-by-step proof of\(\alpha\) from \(\Gamma\). If successful, this shows of course that\(\Gamma\) derives—proves—\(\alpha\), a fact we denote bywriting \(\Gamma \vdash \alpha\). Other reasoning programs may insteadopt for a moreindirect approach and try to establishthat \(\Gamma \vDash \alpha\) by showing that \(\Gamma \cup\{{\sim}\alpha \}\) is inconsistent which, in turn, is shown byderiving a contradiction, \(\bot\), from the set \(\Gamma \cup\{{\sim}\alpha \}\). Automated systems that implement the formerapproach include natural deduction systems; the latter approach isused by systems based on resolution, sequent deduction, and matrixconnection methods.

Soundness and completeness are two (metatheoretical) properties of acalculus that are particularly important for automated deduction.Soundness states that the rules of the calculus aretruth-preserving. For a direct calculus this means that if \(\Gamma\vdash \alpha\) then \(\Gamma \vDash \alpha\). For indirect calculi,soundness means that if \(\Gamma \cup \{{\sim}\alpha \} \vdash \bot\)then \(\Gamma \vDash \alpha\).Completeness in adirect calculus states that if \(\Gamma \vDash \alpha\) then \(\Gamma\vdash \alpha\). For indirect calculi, the completeness property isexpressed in terms ofrefutations since oneestablishes that \(\Gamma \vDash \alpha\) by showing the existence ofa proof, not of \(\alpha\) from \(\Gamma\), but of \(\bot\) from\(\Gamma \cup \{{\sim}\alpha \}\). Thus, an indirect calculus isrefutation complete if \(\Gamma \vDash \alpha\)implies \(\Gamma \cup \{{\sim}\alpha \} \vdash \bot\). Of the twoproperties, soundness is the most desirable. An incomplete calculusindicates that there are entailment relations that cannot beestablished within the calculus. For an automated reasoning programthis means, informally, that there are true statements that theprogram cannot prove. Incompleteness may be an unfortunate affair butlack of soundness is a truly problematic situation since an unsoundreasoning program would be able to generate false conclusions fromperfectly true information.

It is important to appreciate the difference between a logicalcalculus and its corresponding implementation in a reasoning program.The implementation of a calculus invariably involves making somemodifications to the calculus and this results, strictly speaking, ina new calculus. The most important modification to the originalcalculus is the “mechanization” of its deduction rules,that is, the specification of the systematic way in which the rulesare to be applied. In the process of doing so, one must exercise careto preserve the metatheoretical properties of the originalcalculus.

Two other metatheoretical properties of importance to automateddeduction are decidability and complexity. A calculus isdecidable if it admits an algorithmic representation,that is, if there is an algorithm that, for any given \(\Gamma\) and\(\alpha\), it can determine in a finite amount of time the answer,“Yes” or “No”, to the question “Does\(\Gamma \vDash \alpha\)?” A calculus may be undecidable inwhich case one needs to determine which decidable fragment toimplement. The time-spacecomplexity of a calculusspecifies how efficient its algorithmic representation is. Automatedreasoning is made the more challenging because many calculi ofinterest are not decidable and have poor complexity measures forcingresearchers to seek tradeoffs between deductive power versusalgorithmic efficiency.

2.1 Resolution

Of the many calculi used in the implementation of reasoning programs,the ones based on theresolution principle have beenthe most popular. Resolution is modeled after the chain rule (of whichModus Ponens is a special case) and essentially states that from \(p\vee q\) and \({\sim}q \vee r\) one can infer \(p \vee r\). Moreformally, let \(C - l\) denote the clause \(C\) with the literal \(l\)removed. Assume that \(C_1\) and \(C_2\) are ground clausescontaining, respectively, a positive literal \(l_1\) and a negativeliteral \({\sim}l_2\) such that \(l_1\) and \({\sim}l_2\) arecomplementary. Then, the rule ofground resolutionstates that, as a result ofresolving \(C_1\) and\(C_2\), one can infer \((C_1 - l_1) \vee(C_2 - {\sim}l_2)\):

Herbrand’s theorem (Herbrand 1930) assures usthat the non-satisfiability ofany set of clauses, ground ornot, can be established by using ground resolution. This is a verysignificant result for automated deduction since it tells us that if aset \(\Gamma\) is not satisfied by any of the infinitely manyinterpretations, this fact can be determined infinitely manysteps. Unfortunately, a direct implementation of ground resolutionusing Herbrand’s theorem requires the generation of a vastnumber of ground terms making this approach hopelessly inefficient.This issue was effectively addressed by generalizing the groundresolution rule tobinary resolution and byintroducing the notion of unification (Robinson 1965a). Unificationallows resolution proofs to be “lifted” and be conductedat a more general level; clauses only need to be instantiated at themoment where they are to be resolved. Moreover, the clauses resultingfrom the instantiation process do not have to be ground instances andmay still contain variables. The introduction of binary resolution andunification is considered one of the most important developments inthe field of automated reasoning.

Unification

Aunifier of two expressions—terms orclauses—is a substitution that when applied to the expressionsmakes them equal. For example, the substitution \(\sigma\) givenby

is a unifier for

and

since when applied to both expressions it makes them equal:

Amost general unifier (mgu) produces the mostgeneral instance shared by two unifiable expressions. In the previousexample, the substitution \(\{x \leftarrow b, y \leftarrow b, z\leftarrow f(a,b)\}\) is a unifier but not an mgu; however, \(\{x\leftarrow b, z \leftarrow f(a,y)\}\) is an mgu. Note that unificationattempts to “match” two expressions and this fundamentalprocess has become a central component of most automated deductionprograms, resolution-based and otherwise.Theory-unification is an extension of the unificationmechanism that includes built-in inference capabilities. For example,the clauses \(R(g(a,b),x)\) and \(R(g(b,a),d)\) do not unify but theyAC-unify, where AC-unification is unification with built-inassociative and commutative rules such as \(g(a,b) = g(b,a)\).Shifting inference capabilities into the unification mechanism addspower but at a price: The existence of an mgu for two unifiableexpressions may not be unique (there could actually be infinitelymany), and the unification process becomes undecidable in general.

Binary resolution

Let \(C_1\) and \(C_2\) be two clauses containing, respectively, apositive literal \(l_1\) and a negative literal \({\sim}l_2\) suchthat \(l_1\) and \(l_2\) unify with mgu \(\theta\). Then,

by binary resolution; the clause \((C_1\theta - l_1\theta) \vee(C_2\theta - {\sim}l_2\theta)\) is called abinaryresolvent of \(C_1\) and \(C_2\).

Factoring

If two or more literals occurring in a clause \(C\) share an mgu\(\theta\) then \(C\theta\) is afactor of \(C\). Forexample, in \(R(x,a) \vee{\sim}K(f(x),b) \vee R(c,y)\) the literals\(R(x,a)\) and \(R(c,y)\) unify with mgu \(\{x \leftarrow c, y\leftarrow a\}\) and, hence, \(R(c,a) \vee{\sim}K(f(c),b)\) is afactor of the original clause.

The Resolution Principle

Let \(C_1\)and \(C_2\) be two clauses. Then, aresolvent obtained byresolutionfrom \(C_1\) and \(C_2\) is defined as: (a) a binary resolvent of\(C_1\) and \(C_2\); (b) a binary resolvent of \(C_1\) and a factor of\(C_2\); (c) a binary resolvent of a factor of \(C_1\) and \(C_2\);or, (d) a binary resolvent of a factor of \(C_1\) and a factor of\(C_2\).

Resolution proofs, more precisely refutations, are constructed byderiving the empty clause [ ] from \(\Gamma \cup \{{\sim}\alpha\}\) using resolution; this will always be possible if \(\Gamma \cup\{{\sim}\alpha \}\) is unsatisfiable since resolution is refutationcomplete (Robinson 1965a). As an example of a resolution proof, weshow that the set \(\{\forall x(P(x) \vee Q(x)), \forall x(P(x)\supset R(x)),\forall x(Q(x) \supset R(x))\}\), denoted by \(\Gamma\),entails the formula \(\exists xR(x)\). The first step is to find theclausal form of \(\Gamma \cup \{{\sim}\exists xR(x)\}\); the resultingclause set, denoted by \(S_0\), is shown in steps 1 to 4 in therefutation below. The refutation is constructed by using alevel-saturation method: Compute all the resolvents of the initialset, \(S_0\), add them to the set and repeat the process until theempty clause is derived. (This produces the sequence of increasinglylarger sets: \(S_0, S_1, S_2,\ldots)\) The only constraint that weimpose is that we do not resolve the same two clauses more thanonce.

\(S_0\)	1	\(P(x) \vee Q(x)\)	Assumption
	2	\({\sim}\)P\((x) \vee R(x)\)	Assumption
	3	\({\sim}\)Q\((x) \vee R(x)\)	Assumption
	4	\({\sim}R(a)\)	Negate conclusion
\(S_1\)	5	\(Q(x) \vee R(x)\)	Res 1 2
	6	\(P(x) \vee R(x)\)	Res 1 3
	7	\({\sim}P(a)\)	Res 2 4
	8	\({\sim}Q(a)\)	Res 3 4
\(S_2\)	9	\(Q(a)\)	Res 1 7
	10	\(P(a)\)	Res 1 8
	11	\(R(x)\)	Res 2 6
	12	\(R(x)\)	Res 3 5
	13	\(Q(a)\)	Res 4 5
	14	\(P(a)\)	Res 4 6
	15	\(R(a)\)	Res 5 8
	16	\(R(a)\)	Res 6 7
\(S_3\)	17	\(R(a)\)	Res 2 10
	18	\(R(a)\)	Res 2 14
	19	\(R(a)\)	Res 3 9
	20	\(R(a)\)	Res 3 13
	21	[ ]	Res 4 11

Although the resolution proof is successful in deriving [ ], ithas some significant drawbacks. To start with, the refutation is toolong as it takes 21 steps to reach the contradiction, [ ]. Thisis due to the naïve brute-force nature of the implementation. Theapproach not only generates too many formulas but some are clearlyredundant. Note how \(R(a)\) is derived six times; also, \(R(x)\) hasmore “information content” than \(R(a)\) and one shouldkeep the former and disregard the latter. Resolution, like all otherautomated deduction methods, must be supplemented by strategies aimedat improving the efficiency of the deduction process. The above samplederivation has 21 steps but research-type problems command derivationswith thousands or hundreds of thousands of steps.

Resolution Strategies

The successful implementation of a deduction calculus in an automatedreasoning program requires the integration of search strategies thatreduce the search space by pruning unnecessary deduction paths. Somestrategies remove redundant clauses or tautologies as soon as theyappear in a derivation. Another strategy is to remove more specificclauses in the presence of more general ones by a process known assubsumption (Robinson 1965a). Unrestrictedsubsumption, however, does not preserve the refutation completeness ofresolution and, hence, there is a need to restrict its applicability(Loveland 1978).Model elimination (Loveland 1969)can discard a sentence by showing that it is false in some model ofthe axioms. The subject of model generation has received muchattention as a complementary process to theorem proving. The methodhas been used successfully by automated reasoning programs to show theindependence of axioms sets and to determine the existence of discretemathematical structures meeting some given criteria.

Instead of removing redundant clauses, some strategies prevent thegeneration of useless clauses in the first place. Theset-of-support strategy (Wos, Carson & Robinson1965) is one of the most powerful strategies of this kind. A subset\(T\) of the set \(S\), where \(S\) is initially \(\Gamma \cup\{{\sim}\alpha \}\), is called aset of support of\(S\) iff \(S - T\) is satisfiable. Set-of-support resolution dictatesthat the resolved clauses are not both from \(S - T\). The motivationbehind set-of-support is that since the set \(\Gamma\) is usuallysatisfiable it might be wise not to resolve two clauses from\(\Gamma\) against each other.Hyperresolution(Robinson 1965b) reduces the number of intermediate resolvents bycombining several resolution steps into a single inference step.

Independently co-discovered,linear resolution(Loveland 1970, Luckham 1970) always resolves a clause against themost recently derived resolvent. This gives the deduction a simple“linear” structure affording a straightforwardimplementation; yet, linear resolution preserves refutationcompleteness. Using linear resolution we can derive the empty clausein the above example in only eight steps:

1	\(P(x) \vee Q(x)\)	Assumption
2	\({\sim}\)P\((x) \vee R(x)\)	Assumption
3	\({\sim}\)Q\((x) \vee R(x)\)	Assumption
4	\({\sim}R(a)\)	Negated conclusion
5	\({\sim}P(a)\)	Res 2 4
6	\(Q(a)\)	Res 1 5
7	\(R(a)\)	Res 3 6
8	[ ]	Res 4 7

With the exception of unrestricted subsumption, all the strategiesmentioned so far preserve refutation completeness. Efficiency is animportant consideration in automated reasoning and one may sometimesbe willing to trade completeness for speed.Unitresolution andinput resolution are two suchrefinements of linear resolution. In the former, one of the resolvedclauses is always a literal; in the latter, one of the resolvedclauses is always selected from the original set to be refuted. Albeitefficient, neither strategy is complete. Ordering strategies imposesome form of partial ordering on the predicate symbols, terms,literals, or clauses occurring in the deduction.Orderedresolution treats clauses not as sets of literals but assequences—linear orders—of literals. Ordered resolution isextremely efficient but, like unit and input resolution, is notrefutation complete. To end, it must be noted that some strategiesimprove certain aspects of the deduction process at the expense ofothers. For instance, a strategy may reduce the size of the proofsearch space at the expense of increasing, say, the length of theshortest refutations. A taxonomy and detailed presentation oftheorem-proving strategies can be found in Bonacina 1999; for adiscussion of the relative complexity (i.e. efficiency measures) ofresolution see Buresh-Oppenheim & Pitassi 2003, and Urquhart1987.

There are several automated reasoning programs that are based onresolution, or refinements of resolution. Otter (succeeded by Prover4)was a driving force in the development of automated reasoning (Wos,Overbeek, Lusk & Boyle 1984) but it has been superseded by morecapable programs like Vampire (Voronkov 1995, Kovács &Voronkov 2013). Resolution also provides the underlyinglogico-computational mechanism for the popular logic programminglanguage Prolog (Clocksin & Mellish 1981).

2.2 Sequent Deduction

Hilbert-style calculi (Hilbert and Ackermann 1928) have beentraditionally used to characterize logic systems. These calculiusually consist of a few axiom schemata and a small number of rulesthat typically include modus ponens and the rule of substitution.Although they meet the required theoretical requisites (soundness,completeness, etc.) the approach at proof construction in thesecalculi is difficult and does not reflect standard practice. It wasGentzen’s goal “to set up a formalism that reflects asaccurately as possible the actual logical reasoning involved inmathematical proofs” (Gentzen 1935). To carry out this task,Gentzen analyzed the proof-construction process and then devised twodeduction calculi for classical logic: the natural deduction calculus,\(\mathbf{NK}\), and the sequent calculus, \(\mathbf{LK}\). (Gentzenactually designed NK first and then introduced LK to pursuemetatheoretical investigations). The calculi met his goal to a largeextent while at the same time managing to secure soundness andcompleteness. Both calculi are characterized by a relatively largernumber of deduction rules and a simple axiom schema. Of the twocalculi, LK is the one that has been most widely used inimplementations of automated reasoning programs, and it is the onethat we will discuss first; NK will be discussed in the nextsection.

Although the application of the LK rules affect logic formulas, therules are seen as manipulating not logic formulas themselves butsequents.Sequents are expressions of the form\(\Gamma \rightarrow \Delta\), where both \(\Gamma\) and \(\Delta\)are (possibly empty) sets of formulas. \(\Gamma\) is thesequent’santecedent and \(\Delta\) itssuccedent. Sequents can be interpreted thus: Let\(\mathcal{I}\) be an interpretation. Then,

\(\mathcal{I}\) satisfies the sequent \(\Gamma \rightarrow \Delta\)(written as: \(\mathcal{I} \vDash \Gamma \rightarrow \Delta)\) iff
either \(\mathcal{I} \not\vDash \alpha\) (for some \(\alpha \in\Gamma)\) or \(\mathcal{I} \vDash \beta\) (for some \(\beta \in\Delta)\).

In other words,

\(\mathcal{I} \vDash \Gamma \rightarrow \Delta\) iff \(\mathcal{I}\vDash(\alpha_1~ \amp \ldots \amp ~\alpha_n) \supset (\beta_1 \vee\ldots \vee \beta_n)\), where \(\alpha_1~ \amp \ldots \amp ~\alpha_n\)is the iterated conjunction of the formulas in \(\Gamma\) and\(\beta_1 \vee \ldots \vee \beta_n\) is the iterated disjunction ofthose in \(\Delta\).

If \(\Gamma\) or \(\Delta\) are empty then they are respectively validor unsatisfiable. Anaxiom of LK is a sequent\(\Gamma \rightarrow \Delta\) where \(\Gamma \cap \Delta \ne\varnothing\). Thus, the requirement that the same formula occurs ateach side of the \(\rightarrow\) sign means that the axioms of LK arevalid, for no interpretation can then make all the formulas in\(\Gamma\) true and, simultaneously, make all those in \(\Delta\)false. LK has two rules per logical connective, plus one extra rule:the cut rule.

The sequents above a rule’s line are called therule’s premises and the sequent below the lineis therule’s conclusion. The quantificationrules \(\exists \rightarrow\) and \(\rightarrow \forall\) have aneigenvariable condition that restricts their applicability, namelythat \(a\) must not occur in \(\Gamma , \Delta\) or in the quantifiedsentence. The purpose of this restriction is to ensure that the choiceof parameter, \(a\), used in the substitution process is completely“arbitrary”.

Proofs in LK are represented as trees where each node in the tree islabeled with a sequent, and where the original sequent sits at theroot of the tree. The children of a node are the premises of the rulebeing applied at that node. The leaves of the tree are labeled withaxioms. Here is the LK-proof of \(\exists xR(x)\) from the set\(\{\forall x(P(x) \vee Q(x)), \forall x(P(x) \supset R(x)),\forallx(Q(x) \supset R(x))\}\). In the tree below, \(\Gamma\) stands forthis set:

In our example, all the leaves in the proof tree are labeled withaxioms. This establishes the validity of \(\Gamma \rightarrow \existsxR(x)\) and, hence, the fact that \(\Gamma \vDash \exists xR(x)\). LKtakes an indirect approach at proving the conclusion and this is animportant difference between LK and NK. While NK constructs an actualproof (of the conclusion from the given assumptions), LK insteadconstructs a proof that proves the existence of a proof (of theconclusion from the assumptions). For instance, to prove that\(\alpha\) is entailed by \(\Gamma\), NK constructs a step-by-stepproof of \(\alpha\) from \(\Gamma\) (assuming that one exists); incontrast, LK first constructs the sequent \(\Gamma \rightarrow\alpha\) which then attempts to prove valid by showing that it cannotbe made false. This is done by searching for a counterexample thatmakes (all the sentences in) \(\Gamma\) true and makes \(\alpha\)false: If the search fails then a counterexample does not exist andthe sequent is therefore valid. In this respect, proof trees in LK areactually refutation proofs. Like resolution, LK is refutationcomplete: If \(\Gamma \vDash \alpha\) then the sequent \(\Gamma\rightarrow \alpha\) has a proof tree.

As it stands, LK is unsuitable for automated deduction and there aresome obstacles that must be overcome before it can be efficientlyimplemented. The reason is, of course, that the statement of thecompleteness of LK only has to assert, for each entailment relation,the existence of a proof tree but a reasoning program has the moredifficult task of actually having to construct one. Some of the mainobstacles: First, LK does not specify the order in which the rulesmust be applied in the construction of a proof tree. Second, and as aparticular case of the first problem, the premises in the rules\(\forall \rightarrow\) and \(\rightarrow \exists\) rules inherit thequantificational formula to which the rule is applied, meaning thatthe rules can be applied repeatedly to the same formula sending theproof search into an endless loop. Third, LK does not indicate whichformula must be selected next in the application of a rule. Fourth,the quantifier rules provide no indication as to what terms or freevariables must be used in their deployment. Fifth, and as a particularcase of the previous problem, the application of a quantifier rule canlead into an infinitely long tree branch because the proper term to beused in the instantiation never gets chosen. Fortunately, as we willhint at below each of these problems can be successfullyaddressed.

Axiom sequents in LK are valid, and the conclusion of a rule is validiff its premises are. This fact allows us to apply the LK rules ineither direction, forwards from axioms to conclusion, or backwardsfrom conclusion to axioms. Also, with the exception of the cut rule,all the rules’ premises are subformulas of their respectiveconclusions. For the purposes of automated deduction this is asignificant fact and we would want to dispense with the cut rule;fortunately, the cut-free version of LK preserves its refutationcompleteness (Gentzen 1935). These results provide a strong case forconstructing proof trees in a backwards fashion; indeed, by workingthis way a refutation in cut-free LK gets increasingly simpler as itprogresses since subformulas are simpler than their parent formulas.Moreover, and as far as propositional rules go, the new subformulasentered into the tree are completely dictated by the cut-free LKrules. Furthermore, and assuming the proof tree can be brought tocompletion, branches eventually end up with atoms and the presence ofaxioms can be quickly determined. Another reason for working backwardsis that the truth-functional fragment of cut-free LK isconfluent in the sense that the order in which thenon-quantifier rules are applied is irrelevant: If there is a proof,regardless of what you do, you will run into it! To bring thequantifier rules into the picture, things can be arranged so that allrules have a fair chance of being deployed: Apply, as far as possible,all the non-quantifier rules before applying any of the quantifierrules. This takes care of the first and second obstacles, and it is notoo difficult to see how the third one would now be handled. Thefourth and fifth obstacles can be addressed by requiring that theterms to be used in the substitutions be suitably selected from theHerbrand universe (Herbrand 1930).

The use of sequent-type calculi in automated theorem proving wasinitiated by efforts to mechanize mathematics (Wang 1960). At thetime, resolution captured most of the attention of the automatedreasoning community but during the 1970s some researchers started tofurther investigate non-resolution methods (Bledsoe 1977), prompting afrutiful and sustained effort to develop more human-oriented theoremproving systems (Bledsoe 1975, Nevins 1974). Eventually, sequent-typededuction gained momentum again, particularly in its re-incarnation asanalytic tableaux (Fitting 1990). The method ofdeduction used in tableaux is essentially cut-free LK’s withsets used in lieu of sequents.

2.3 Natural Deduction

Although LK and NK are both commonly labeled as “naturaldeduction” systems, it is the latter which better deserves thetitle due to its more natural, human-like, approach to proofconstruction. The rules of NK are typically presented as acting onstandard logic formulas in an implicitly understood context, but theyare also commonly given in the literature as acting more explicitly on“judgements”, that is, expressions of the form \(\Gamma\vdash \alpha\) where \(\Gamma\) is a set of formulas and \(\alpha\)is a formula. This form is typically understood as making themetastatement that there is a proof of \(\alpha\) from \(\Gamma\)(Kleene 1962). Following Gentzen 1935 and Prawitz 1965 here we takethe former approach. The system NK has no logical axioms and providestwo introduction-elimination rules for each logical connective:

A few remarks: First, the expression [\(\alpha\)—\( \gamma\)]represents the fact that \(\alpha\) is an auxiliary assumption in theproof of \(\gamma\) that eventually gets discharged, i.e. discarded.For example, \(\exists\)E tells us that if in the process ofconstructing a proof one has already derived \(\exists x\alpha(x)\)and also \(\beta\) with \(\alpha(a/x)\) as an auxiliary assumptionthen the inference to \(\beta\) is allowed. Second, theeigenparameter, \(a\), in \(\exists\)E and \(\forall\)I must beforeign to the premises,undischarged—“active”—assumptions, to therule’s conclusion and, in the case of \(\exists\)E, to \(\existsx\alpha(x)\). Third, \(\bot\) is shorthand for two contradictoryformulas, \(\beta\) and \({\sim}\beta\). Finally, NK is complete: If\(\Gamma \vDash \alpha\) then there is a proof of \(\alpha\) from\(\Gamma\) using the rules of NK.

As in LK, proofs constructed in NK are represented as trees with theproof’s conclusion sitting at the root of the tree, and theproblem’s assumptions sitting at the leaves. (Proofs are alsotypically given as sequences of judgements, \(\Gamma \vdash \alpha\),running from the top to the bottom of the printed page.) Here is anatural deduction proof tree of \(\exists xR(x)\) from \(\forallx(P(x) \vee Q(x)), \forall x(P(x) \supset R(x))\) and \(\forall x(Q(x)\supset R(x))\):

As in LK, a forward-chaining strategy for proof construction is notwell focused. So, although proofs areread forwards, that is,from leaves to root or, logically speaking, from assumptions toconclusion, that is not the way in which they are typicallyconstructed. A backward-chaining strategy implemented byapplying the rules in reverse order is more effective. Many of theobstacles that were discussed above in the implementation of sequentdeduction are applicable to natural deduction as well. These issuescan be handled in a similar way, but natural deduction introduces someissues of its own. For example, as suggested by the\(\supset\)-Introduction rule, to prove a goal of the form \(\alpha\supset \beta\) one could attempt to prove \(\beta\) on the assumptionthat \(\alpha\). But note that although the goal \(\alpha \supset\beta\) does not match the conclusion of any other introduction rule,it matches the conclusion of allelimination rules and thereasoning program would need to consider those routes too. Similarlyto forward-chaining, here there is the risk of setting goals that areirrelevant to the proof and that could lead the program astray. Towit: What prevents a program from entering the never-ending process ofbuilding, say, larger and larger conjunctions? Or, what is there toprevent an uncontrolled chain of backward applications of, say,\(\supset\)-Elimination? Fortunately, NK enjoys thesubformulaproperty in the sense that each formula entering into anatural deduction proof can be restricted to being a subformula of\(\Gamma \cup \Delta \cup \{\alpha \}\), where \(\Delta\) is the setof auxiliary assumptions made by the \({\sim}\)-Elimination rule. Byexploiting the subformula property a natural deduction automatedtheorem prover can drastically reduce its search space and bring thebackward application of the elimination rules under control (Portoraro1998, Sieg & Byrnes 1996). Further gains can be realized if one iswilling to restrict the scope of NK’s logic to itsintuitionistic fragment where every proof has a normal form in thesense that no formula is obtained by an introduction rule and then iseliminated by an elimination rule (Prawitz 1965).

Implementations of automated theorem proving systems using NKdeduction have been motivated by the desire to have the program reasonwith precisely the same proof format and methods employed by the humanuser. This has been particularly true in the area of education wherethe student is engaged in the interactive construction of formalproofs in an NK-like calculus working under the guidance of a theoremprover ready to provide assistance when needed (Portoraro 1994, Suppes1981). Other, research-oriented, theorem provers true to the spirit ofNK exist (Pelletier 1998) but are rare.

2.4 The Matrix Connection Method

The name of the matrix connection method (Bibel 1981) is indicative ofthe way it operates. The term “matrix” refers to the formin which the set of logic formulas expressing the problem isrepresented; the term “connection” refers to the way themethod operates on these formulas. To illustrate the method at work,we will use an example from propositional logic and show that \(R\) isentailed by \(P \vee Q, P \supset R\) and \(Q \supset R\). This isdone by establishing that the formula

is unsatisfiable. To do this, we begin by transforming it intoconjunctive normal form:

This formula is then represented as a matrix, one conjunct per rowand, within a row, one disjunct per column:

The idea now is to explore all the possible vertical paths runningthrough this matrix. Avertical path is a set ofliterals selected from each row in the matrix such that each literalcomes from a different row. The vertical paths:

A path iscomplementary if it contains two literalswhich are complementary. For example, Path 2 is complementary since ithas both \(P\) and \({\sim}P\) but so is Path 6 since it contains both\(R\) and \({\sim}R\). Note that as soon as a path includes twocomplementary literals there is no point in pursuing the path since ithas itself become complementary. This typically allows for a largereduction in the number of paths to be inspected. In any event, allthe paths in the above matrix are complementary and this factestablishes the unsatisfiability of the original formula. This is theessence of the matrix connection method. The method can be extended topredicate logic but this demands additional logical apparatus:Skolemnization, variable renaming, quantifier duplication,complementarity of paths via unification, and simultaneoussubstitution across all matrix paths (Bibel 1981, Andrews 1981).Variations of the method have been implemented in reasoning programsin higher-order logic (Andrews 1981) and non-classical logics (Wallen1990).

2.5 Term Rewriting

Equality is an important logical relation whose behavior withinautomated deduction deserves its own separate treatment.Equational logic and, more generally,termrewriting treat equality-like equations asrewriterules, also known asreduction ordemodulation rules. An equality statement like\(f(a)= a\) allows the simplification of a term like \(g(c,f(a))\) to\(g(c,a)\). However, the same equation also has the potential togenerate an unboundedly large term: \(g(c,f(a)), g(c,f(f(a))),g(c,f(f(f(a)))),\ldots\) . What distinguishes term rewriting fromequational logic is that in term rewriting equations are used asunidirectional reduction rules as opposed to equality which works inboth directions. Rewrite rules have the form \(t_1 \Rightarrow t_2\)and the basic idea is to look for terms \(t\) occurring in expressions\(e\) such that \(t\) unifies with \(t_1\) with unifier \(\theta\) sothat the occurrence \(t_1\theta\) in \(e\theta\) can be replaced by\(t_2\theta\). For example, the rewrite rule \(x + 0 \Rightarrow x\)allows the rewriting ofsucc(succ(0) \(+ 0)\) assucc(succ(0)).

To illustrate the main ideas in term rewriting, let us explore anexample involving symbolic differentiation (the example and ensuingdiscussion are adapted from Chapter 1 of Baader & Nipkow 1998).Letder denote the derivative respect to \(x\), let \(y\) bea variable different from \(x\), and let \(u\) and \(v\) be variablesranging over expressions. We define the rewrite system:

Again, the symbol \(\Rightarrow\) indicates that a term matching theleft-hand side of a rewrite rule should be replaced by therule’s right-hand side. To see the differentiation system atwork, let us compute the derivative of \(x \times x\) respect to\(x\), \(\der(x \times x)\):

At this point, since none of the rules (R1)–(R4) applies, nofurther reduction is possible and the rewriting process ends. Thefinal expression obtained is called anormal form,and its existence motivates the following question: Is there anexpression whose reduction process will never terminate when applyingthe rules (R1)–(R4)? Or, more generally: Under what conditions aset of rewrite rules will always stop, for any given expression, at anormal form after finitely many applications of the rules? Thisfundamental question is called theterminationproblem of a rewrite system, and we state without proof that thesystem (R1)–(R4) meets the termination condition.

There is the possibility that when reducing an expression, the set ofrules of a rewrite system could be applied in more than one way. Thisis actually the case in the system (R1)–(R4) where in thereduction of \(\der(x \times x)\) we could have applied R1 first tothe second sub-expression in \((x \times\) \(\der(x)) + \der(x) \timesx)\), as shown below:

Following this alternative course of action, the reduction terminateswith the same normal form as in the previous case. This fact, however,should not be taken for granted: A rewriting system is said to be(globally) confluent if and only if independently ofthe order in which its rules are applied every expression always endsup being reduced to its one and only normal form. It can be shown that(R1)–(R4) is confluent and, hence, we are entitled to say:“Computethe derivative of an expression” (asopposed to simply “\(a\)” derivative). Adding more rulesto a system in an effort to make it more practical can have undesiredconsequences. For example, if we add the rule

to (R1)–(R4) then we will be able to further reduce certainexpressions but at the price of losing confluency. The followingreductions show that \(\der(x + 0)\) now has two normal forms: thecomputation

gives one normal form, and

gives another. Adding the rule

would allow the further reduction of \(1 + \der(0)\) to \(1 + 0\) andthen, by R5, to 1. Although the presence of this new rule actuallyincreases the number of alternative paths—\(\der(x + 0)\) cannow be reduced in four possible ways—they all end up with thesame normal form, namely 1. This is no coincidence as it can be shownthat (R6) actually restores confluency. This motivates anotherfundamental question: Under what conditions can a non-confluent systembe made into an equivalent confluent one? The Knuth-Bendixcompletion algorithm (Knuth & Bendix 1970) givesa partial answer to this question.

Term rewriting, like any other automated deduction method, needsstrategies to direct its application. Rippling (Bundy, Stevens &Harmelen 1993, Basin & Walsh 1996) is a heuristic that has itsorigins in inductive theorem-proving that uses annotations toselectively restrict the rewriting process. Thesuperpositioncalculus is a calculus of equational first-order logic thatcombines notions from first-order resolution and Knuth-Bendix orderingequality. Superposition is refutation complete (Bachmair &Ganzinger 1994) and is at the heart of a number of theorem provers,most notably the E equational theorem prover (Schulz 2004) and Vampire(Voronkov 1995). Superposition has been extended to higher-order logic(Bentkampet al. 2021).

2.6 Mathematical Induction

Mathematical induction is a very important technique of theoremproving in mathematics and computer science. Problems stated in termsof objects or structures that involve recursive definitions or someform of repetition invariably require mathematical induction for theirsolving. In particular, reasoning about the correctness of computersystems requires induction and an automated reasoning program thateffectively implements induction will have important applications.

To illustrate the need for mathematical induction, assume that aproperty \(\phi\) is true of the number zero and also that if true ofa number then is true of its successor. Then, with our deductivesystems, we can deduce that for any given number \(n, \phi\) is trueof it, \(\phi(n)\). But we cannot deduce that \(\phi\) is true of allnumbers, \(\forall x\phi(x)\); this inference step requires the ruleof mathematical induction:

In other words, to prove that \(\forall x\alpha(x)\) one proves that\(\alpha(0)\) is the case, and that \(\alpha(succ(n))\) follows fromthe assumption that \(\alpha(n)\). The implementation of induction ina reasoning system presents very challenging search control problems.The most important of these is the ability to determine the particularway in which induction will be applied during the proof, that is,finding the appropriate induction schema. Related issues includeselecting the proper variable of induction, and recognizing all thepossible cases for the base and the inductive steps.

The Boyer-Moore theorem prover (Boyer & Moore 1979) has been amost successful implementation of automated inductive theorem proving.In the spirit of Gentzen, Boyer and Moore were interested in howpeople prove theorems by mathematical induction. Their theorem proveris written in the functional programming language Lisp which is alsothe language in which theorems are represented. For instance, toexpress the commutativity of addition the user would enter the Lispexpression(EQUAL (PLUS X Y) (PLUS Y X)).Everything defined in the system is a functional term, including itsbasic “predicates”:T,F,EQUAL X Y,ANDX Y,NOT X,IFX Y Z, etc. Proofs are conducted by rewritingterms that possess recursive definitions, ultimately reducing theconclusion’s statement to theTpredicate. The Boyer-Moore theorem prover has been used to check theproofs of some quite deep theorems (Boyer, Kaufmann & Moore 1995).Lemma caching, problem statement generalization, and proof planningare techniques particularly useful in inductive theorem proving(Bundy, Harmelen & Hesketh 1991).

ACL2 (Kaufmann & Moore 1996) is a successor of, and supersedes,the Boyer-Moore prover and is intended for large-scale hardware andsoftware verification projects. Models of computer hardware andsoftware can be formally represented as “state machines”consisting of “states” as mathematical objects and“transitions” as functions or relations on state objects.ACL2 uses an extension of an applicative subset of Common Lisp as thenatural language in which to express such notions and where models andtheir properties can be derived logically (Boyer & Moore 1997).ACL2 supports the user in the building of proofs but its primary roleis to prevent logical mistakes. In a quasi-“black box”fashion, “to be a good user of ACL2 you do not have tounderstand how the theorem prover works. You just have to understandhow to interact with it” (Kaufmann & Moore 2024 [OtherInternet Resources]) but, if desired, the user can easily command ACL2to supply its full proof output for inspection. The authors of ACL2share the interesting insight that ACL2 users rarely read successfulproofs and tend to concentrate on subgoals in failed proofs; then,they try to figure out how these goals could be proved and provideACL2 with guidance to do so. Although ACL2 has been largely applied tothe formal verification of microprocessor design (see the section4.4 Formal Verification of Hardware) ACL2 has found manyapplications in other areas of which we mention three here: theformalization of the Normalization Theorem in algebraic simplicialtopology (Lambán, Martín-Mateos, Rubio & Ruiz-Reina2012), the formal verification of an implementation ofBuchberger’s algorithm for computing Gröbner bases ofpolynomial ideals (Medina-Bulo, Palomo-Lozano & Ruiz-Reina 2010),and a formalization of finite group theory up to an application of theSylow theorems (Russinoff 2023).

3. Other Logics

3.1 Higher-Order Logic

Higher-order logic differs from first-order logic in thatquantification over functions and predicates is allowed. The statement“Any two people are related to each other in one way oranother” can be legally expressed in higher-order logic as\(\forall x\forall y\exists RR(x,y)\) but not in first-order logic.Higher-order logic is inherently more expressive than first-orderlogic and is closer in spirit to actual mathematical reasoning. Forexample, the notion of set finiteness cannot be expressed as afirst-order concept. Due to its richer expressiveness, it should notcome as a surprise that implementing an automated theorem prover forhigher-order logic is more challenging than for first-order logic.This is largely due to the fact that unification in higher-order logicis more complex than in the first-order case: unifiable terms do notalways possess a most general unifier, and higher-order unification isitself undecidable. Finally, given that higher-order logic isincomplete, there are always proofs that will be entirely out of reachfor any automated reasoning program.

Methods used to automate first-order deduction can be adapted tohigher-order logic. TPS (Andrewset al. 1996, Andrewsetal. 2006) is a theorem proving system for higher-order logic thatuses Church’s typed \(\lambda\)-calculus as its logicalrepresentation language and is based on a connection-type deductionmechanism that incorporates Huet’s unification algorithm (Huet1975). As a sample of the capabilities of TPS, the program has provedautomatically that a subset of a finite set is finite, the equivalenceamong several formulations of the Axiom of Choice, and Cantor’sTheorem that a set has more subsets than members. The latter wasproved by the program by asserting that there is no onto function fromindividuals to sets of individuals, with the proof proceeding by adiagonal argument. HOL (Gordon & Melham 1993) is anotherhigher-order proof development system primarily used as an aid in thedevelopment of hardware and software safety-critical systems. HOL isbased on the LCF approach to interactive theorem proving (Gordon,Milner & Wadsworth 1979), and it is built on the strongly typedfunctional programming language ML. HOL, like TPS, can operate inautomatic and interactive mode. Availability of the latter mode iswelcomed since the most useful automated reasoning systems may well bethose which place an emphasis on interactive theorem proving (Farmer,Guttman & Thayer 1993) and can be used as assistants operatingunder human guidance. (Harrison 2000) discusses the verification offloating-point algorithms and the non-trivial mathematical propertiesthat are proved by HOL Light under the guidance of the user. Isabelle(Paulson 1994) is a generic, higher-order, framework for rapidprototyping of deductive systems. Object logics can be formulatedwithin Isabelle’s metalogic by using its many syntactic anddeductive tools. Isabelle also provides some ready-made theoremproving environments, including Isabelle/HOL, Isabelle/ZF andIsabelle/FOL, which can be used as starting points for applicationsand further development by the user (Paulson 1990, Nipkow &Paulson 2002). Isabelle/ZF has been used to prove equivalentformulations of the Axiom of Choice, formulations of the Well-OrderingPrinciple, as well as the key result about cardinal arithmetic that,for any infinite cardinal \(\kappa , \kappa \cdot \kappa = \kappa\)(Paulson & Grabczewski 1996).

To help prove higher-order theorems and discharge goals arising ininteractive proofs, the user can ask Isabelle/HOL to invoke externalfirst-order provers through Sledgehammer (Paulson 2010), a subsystemaimed at combining the complementary capabilities of automatedreasoning systems of different types, including SMT solvers (seethe section on SAT Solvers; Blanchetteet al. 2013). LEO-II (Benzmülleretal. 2015) is also a resolution-based automated theorem prover forhigher-order logic that has been applied in a wide array of problems,most notably in the automation of Gödel’s ontological proofof God’s existence (see Section 4.6 Logic and Philosophy). Leo-II has been superseded by Leo-III which implements a higher-orderordered paramodulation calculus that operates within a multi-agentblackboard architecture for parallel proof search; the architectureallows to independently run agents using Leo-III’s native proofcalculus as well as, in a cooperative fashion, agents for external,specialized, first- and higher-order theorem provers and model finders(Benzmüller, Steen & Wisniewski 2017, Steen andBenzmüller 2021).

3.2 Non-classical Logics

Non-classical logics (Haack 1978) such as modal logics, intuitionsiticlogic, multi-valued logics, autoepistemic logics, non-monotonicreasoning, commonsense and default reasoning, relevance logic,paraconsistent logic, and so on, have been increasingly gaining theattention of the automated reasoning community. One of the reasons hasbeen the natural desire to extend automated deduction techniques tonew domains of logic. Another reason has been the need to mechanizenon-classical logics as an attempt to provide a suitable foundationfor artificial intelligence. A third reason has been the desire toattack some problems that are combinatorially too large to be handledby paper and pencil. Indeed, some of the work in automatednon-classical logic provides a prime example of automated reasoningprograms at work. To illustrate, the Ackerman Constant Problem asksfor the number of non-equivalent formulas in the relevance logic R.There are actually 3,088 such formulas (Slaney 1984) and the numberwas found by “sandwiching” it between a lower and an upperlimit, a task that involved constraining a vast universe of \(20^{400}20\)-element models in search of those models that rejectednon-theorems in R. It is safe to say that this result would have beenimpossible to obtain without the assistance of an automated reasoningprogram.

There have been three basic approaches to automate the solving ofproblems in non-classical logic (McRobie 1991). One approach has been,of course, to try to mechanize the non-classical deductive calculi.Another has been to simply provide an equivalent formulation of theproblem in first-order logic and let a classical theorem prover handleit. A third approach has been to formulate the semantics of thenon-classical logic in a first-order framework where resolution orconnection-matrix methods would apply. (Pelletieret al.2017) describes an automated reasoning system for a paraconsistentlogic that takes both “indirect” approaches, thetranslational and the truth-value approach, to prove its theorems.

Modal logic

Modal logics find extensive use in computing science as logics ofknowledge and belief, logics of programs, and in the specification ofdistributed and concurrent systems. Thus, a program that automatesreasoning in a modal logic such as K, K4, T, S4, or S5 would haveimportant applications. With the exception of S5, these logics sharesome of the important metatheoretical results of classical logic, suchas cut-elimination, and hence cut-free (modal) sequent calculi can beprovided for them, along with techniques for their automation.Connection methods (Andrews 1981, Bibel 1981) have played an importantrole in helping to understand the source of redundancies in the searchspace induced by these modal sequent calculi and have provided aunifying framework not only for modal logics but also forintuitionistic and classical logic as well (Wallen 1990). Currentefforts to automate modal logic reasoning revolve around thetranslational approach mentioned above, namely to embed modal logicinto classical logic and then use an existing automated reasoningsystem for the latter to prove theorems of the former.(Benzmüller & Paulson 2013) shows how to embed quantifiedmodal logic into simple type theory, proves the soundness andcompleteness of the embedding, and demonstrates with simpleexperiments how existing higher-order theorem provers can be used toautomate proofs in modal logic. The approach can be extended tohigher-order modal logic as well (Benzmüller & Paleo 2015).As a matter of fact, embeddings in classical higher-order logic can beused as a means for universal reasoning (Benzmüller 2019); thatis, the embedding provides a universal logical reasoning frameworkthat uses classical higher-order logic as a metalogic in which variousother classical and non-classical logics can be represented. Furtherevidence to the claim of universality is provided by the semanticalembedding approach to free logic and category theory (Benzmüller& Scott 2020). Embedding yields a number of practical benefits toautomated deduction: universality, uniformity, expressiveness ofnotation and reasoning, and ready availability of existing powerfulautomated theorem-proving tools that are known to be sound.

Intuitionistic logic

There are different ways in which intuitionsitic logic can beautomated. One is to directly implement the intuitionistic versions ofGentzen’s sequent and natural deduction calculi, LJ and NJrespectively. This approach inherits the stronger normalizationresults enjoyed by these calculi allowing for a more compactmechanization than their classical counterparts. Another approach atmechanizing intuitionistic logic is to exploit its semanticsimilarities with the modal logic S4 and piggy back on an automatedimplementation of S4. Automating intuitionistic logic has applicationsin software development since writing a program that meets aspecification corresponds to the problem of proving the specificationwithin an intuitionistic logic (Martin-Löf 1982). A system thatautomated the proof construction process would have importantapplications in algorithm design but also in constructive mathematics.Nuprl (Constableet al. 1986) is a computer system supportinga particular mathematical theory, namely constructive type theory, andwhose aim is to provide assistance in the proof development process.The focus is on logic-based tools to support programming and onimplementing formal computational mathematics. Over the years thescope of the Nuprl project has expanded from“proofs-as-programs” to “systems-as-theories”.Similar in spirit and based on the Curry-Howard isomorphism, the Coqsystem formalizes its proofs in the Calculus of InductiveConstructions, a \(\lambda\)-calculus with a rich system of typesincluding dependent types (Coquand & Huet 1988, Coquand &Paulin-Mohring 1988). Like Nuprl, Coq is designed to assist in thedevelopment of mathematical proofs as well as computer programs fromtheir formal specifications.

4. Applications

4.1 Logic Programming

Logic programming, particularly represented by the languageProlog (Colmeraueret al. 1973), is probablythe most important and widespread application of automated theoremproving. During the early 1970s, it was discovered that logic could beused as a programming language (Kowalski 1974). What distinguisheslogic programming from other traditional forms of programming is thatlogic programs, in order to solve a problem, do not explicitly statehow a specific computation is to be performed; instead, alogic program stateswhat the problem is and then delegatesthe task of actually solving it to an underlying theorem prover. InProlog, the theorem prover is based on a refinement of resolutionknown as SLD-resolution.SLD-resolution is avariation of linear input resolution that incorporates a special rulefor selecting the next literal to be resolved upon; SLD-resolutionalso takes into consideration the fact that, in the computer’smemory, the literals in a clause are actually ordered, that is, theyform a sequence as opposed to a set. A Prologprogramconsists of clauses stating known facts and rules. For example, thefollowing clauses make some assertions about flight connections:

flight(toronto, london).
flight(london, rome).
flight(chicago, london).
flight\((X, Y)\) :– flight\((X, Z)\) , flight\((Z, Y)\).

The clause flight(toronto, london) is a fact while flight\((X, Y)\):– flight\((X, Z)\) , flight\((Z,Y)\) is a rule, written byconvention as a reversed conditional (the symbol“:–” means “if”; the comma means“and”; terms starting in uppercase are variables). Theformer states that there is flight connection between Toronto andLondon; the latter states that there is a flight between cities \(X\)and \(Y\) if, for some city \(Z\), there is a flight between \(X\) and\(Z\) and one between \(Z\) and \(Y\). Clauses in Prolog programs area special type of Horn clauses having precisely one positive literal:Facts are program clauses with no negative literalswhilerules have at least one negative literal. (Notethat in standard clause notation the program rule in the previousexample would be written as flight\((X,Y) \vee{\sim}\)flight\((X,Z)\vee{\sim}\)flight\((Z,Y)\).) The specific form of the program rulesis to effectively express statements of the form: “If theseconditions over here are jointly met then this other fact willfollow”. Finally, agoal is a Horn clausewith no positive literals. The idea is that, once a Prolog program\(\Pi\) has been written, we can then try to determine if a new clause\(\gamma\), the goal, is entailed by \(\Pi , \Pi \vDash \gamma\); theProlog prover does this by attempting to derive a contradiction from\(\Pi \cup \{{\sim}\gamma \}\). We should remark that program factsand rules alone cannot produce a contradiction; a goal must enter intothe process. Like input resolution, SLD-resolution is not refutationcomplete for first-order logic but it is complete for the Horn logicof Prolog programs. The fundamental theorem: If \(\Pi\) is a Prologprogram and \(\gamma\) is the goal clause then \(\Pi \vDash \gamma\)iff \(\Pi \cup \{{\sim}\gamma \} \vdash [\,]\) by SLD-resolution(Lloyd 1984).

For instance, to find out if there is a flight from Toronto to Romeone asks the Prolog prover to see if the clause flight(toronto, rome)follows from the given program. To do this, the prover adds\({\sim}\)flight(toronto,rome) to the program clauses and attempts toderive the empty clause, \([\,]\), by SLD-resolution:

The conditional form of rules in Prolog programs adds to theirreadability and also allows reasoning about the underlying refutationsin a more friendly way: To prove that there is a flight betweenToronto and Rome, flight(toronto,rome), unify this clause with theconsequent flight\((X,Y)\) of the fourth clause in the program whichitself becomes provable if both flight(toronto,\(Z)\) andflight\((Z\),rome) can be proved. This can be seen to be the caseunder the substitution \(\{Z \leftarrow\) london\(\}\) since bothflight(toronto,london) and flight(london,rome) are themselvesprovable. Note that the theorem prover not only establishes that thereis a flight between Toronto and Rome but it can also come up with anactual itinerary, Toronto-London-Rome, by extracting it from theunifications used in the proof.

There are at least two broad problems that Prolog must address inorder to achieve the ideal of a logic programming language. Logicprograms consist of facts and rules describing what is true; anythingthat is not provable from a program is deemed to be false. In regardsto our previous example,flight(toronto,boston) is not true since this literal cannot be deduced fromthe program. The identification of falsity with non-provability isfurther exploited in most Prolog implementations by incorporating anoperator,not, that allows programmers to explicitlyexpress the negation of literals (or even subclauses) within aprogram. By definition, not \(l\) succeeds if the literal \(l\) itselffails to be deduced. This mechanism, known asnegation-by-failure, has been the target ofcriticism. Negation-by-failure does not fully capture the standardnotion of negation and there are significant logical differencesbetween the two. Standard logic, including Horn logic, is monotonicwhich means that enlarging an axiom set by adding new axioms simplyenlarges the set of theorems derivable from it; negation-by-failure,however, isnon-monotonic and the addition of newprogram clauses to an existing Prolog program may cause some goals tocease from being theorems. A second issue is thecontrolproblem. Currently, programmers need to provide a fair amountof control information if a program is to achieve acceptable levels ofefficiency. For example, a programmer must be careful with the orderin which the clauses are listed within a program, or how the literalsare ordered within a clause. Failure to do a proper job can result inan inefficient or, worse, non-terminating program. Programmers mustalso embed hints within the program clauses to prevent the prover fromrevisiting certain paths in the search space (by using thecut operator) or to prune them altogether (by usingfail. Last but not least, in order to improve theirefficiency, many implementations of Prolog do not implementunification fully and bypass a time-consuming yet criticaltest—the so-calledoccurs-check—responsible for checking thesuitability of the unifiers being computed. This results in an unsoundcalculus and may cause a goal to be entailed by a Prolog program (froma computational point of view) when in fact it should not (from alogical point of view).

There are variations of Prolog intended to extend its scope. Byimplementing a model elimination procedure, the Prolog TechnologyTheorem Prover (PTTP) (Stickel 1992) extends Prolog into fullfirst-order logic. The implementation achieves both soundness andcompleteness. Moving beyond first-order logic, \(\lambda\)Prolog(Miller & Nadathur 1988) bases the language on higher-orderconstructive logic.

4.2 SAT Solvers

The problem of determining the satisfiability of logic formulas hasreceived much attention by the automated reasoning community due toits important applicability in industry. A propositional formula issatisfiable if there is an assignment of truth-valuesto its variables that makes the formula true. For example, theassignment \((P \leftarrow\) true, \(Q \leftarrow\) true, \(R\leftarrow\) false) does not make \((P \vee R) \amp{\sim}Q\) true but\((P \leftarrow\) true, \(Q \leftarrow\) false, \(R \leftarrow\)false) does and, hence, the formula is satisfiable. Determiningwhether a formula is satisfiable or not is called the BooleanSatisfiability Problem—\(\mathbf{SAT}\) for short—and fora formula with \(n\) variables SAT can be settled thus: Inspect eachof the \(2^n\) possible assignments to see if there is at least oneassignment that satisfies the formula, i.e. makes it true. This methodis clearly complete: If the original formula is satisfiable then wewill eventually find one such satisfying assignment; but if theformula is contradictory (i.e. non-satisfiable), we will be able todetermine this too. Just as clearly, and particularly in this lattercase, this search takes an exponential amount of time, and the desireto conceive more efficient algorithms is well justified particularlybecause many computing problems of great practical importance such asgraph-theoretic problems, network design, storage and retrieval,scheduling, program optimization, and many others (Garey & Johnson1979) can be expressed as SAT instances, i.e. as the SAT question ofsome propositional formula representing the problem. Given that SAT isNP-complete (Cook 1971) it is very unlikely that a polynomialalgorithm exists for it; however, this does not preclude the existenceof sufficiently efficient algorithms for particular cases of SATproblems.

The Davis-Putnam-Logemann-Loveland \((\mathbf{DPLL})\) algorithm wasone of the first SAT search algorithms (Davis & Putnam 1960;Davis, Logemman & Loveland 1962) and is still considered one ofthe best complete SAT solvers; many of the complete SAT procedures inexistence today can be considered optimizations and generalizations ofDPLL. In essence, DPLL search procedures proceed by considering waysin which assignments can be chosen to make the original formula true.For example, consider the formula in CNF \[P \amp{\sim}Q \amp({\sim}P \vee Q \vee R) \amp(P \vee{\sim}S)\] Since \(P\) is aconjunct, but also a unit clause, \(P\) must be true if the entireformula is to be true. Moreover, the value of \({\sim}P\) does notcontribute to the truth of \({\sim}P \vee Q \vee R\) and \(P\vee{\sim}S\) is true regardless of \(S\). Thus, the whole formulareduces to \[{\sim}Q \amp(Q \vee R)\] Similarly, \({\sim}Q\) must be true and theformula further reduces to \[R\] which forces \(R\) to be true.From this process we can recover the assignment \((P \leftarrow\)true, \(Q \leftarrow\) false, \(R \leftarrow\) true, \(S \leftarrow\)false) proving that the original formula is satisfiable. A formula maycause the algorithm to branch; the search through a branch reaches adead end the moment a clause is deemed false—aconflicting clause—and all variations of theassignment that has been partially constructed up to this point can bediscarded. To illustrate:

Hence, the formula is satisfiable by the existence of \((P\leftarrow\) false, \(Q \leftarrow\) true, \(R \leftarrow\) true).DPLL algorithms are made more efficient by strategies such asterm indexing (ordering of the formula variables inan advantageous way),chronological backtracking(undoing work to a previous branching point if the process leads to aconflicting clause), andconflict-driven learning(determining the information to keep and where to backtrack). Thecombination of these strategies results in a large prune of the searchspace; for a more extensive discussion the interested reader isdirected to Zhang & Malik 2002.

A quick back-envelope calculation reveals the staggering computingtimes of (algorithms for) SAT-type problems represented by formulaswith as little as, say, 60 variables. To wit: A problem represented asa Boolean formula with 10 variables that affords a linear solutiontaking one hundredth of a second to complete would take just fourhundredths and six hundredths of a second to complete if the formulahad instead 40 and 60 variables respectively. In dramatic contrast, ifthe solution to the problem were exponential (say \(2^n)\) then thetimes to complete the job for 10, 40 and 60 variables would berespectively one thousandth of a second, 13 days, and 365 centuries.It is a true testament to the ingenuity of the automated reasoningcommunity and the power of current SAT-based search algorithms thatreal-world problems with thousands of variables can be handled withreasonable efficency. Küchlin & Sinz 2000 discuss a SATapplication in the realm of industrial automotive product datamanagement where 18,000 (elementary) Boolean formulas and 17,000variables are used to express constraints on orders placed bycustomers. As another example, Massacci & Marraro 2000 discuss anapplication in logical cryptanalysis, that is, the verification ofproperties of cryptographic algorithms expressed as SAT problems. Theydemonstrate how finding a key with a cryptographic attack is analogousto finding a model—assignment—for a Boolean formula; theformula in their application encodes the commercial version of the U.SData Encryption Standard (DES) with the encoding requiring 60,000clauses and 10,000 variables.

Although SAT is conceptually very simple, its inner nature is not wellunderstood—there are no criteria that can be generally appliedto answer as to why one SAT problem is harder than another. It shouldthen come as no surprise that algorithms that tend to do well on someSAT instances do not perform so well on others, and efforts are beingspent in designing hybrid algorithmic solutions that combine thestrength of complementary approaches—see Prasad, Biere &Gupta 2005 for an application of this hybrid approach in theverification of hardware design.

Recent advances in SAT hybrid strategies coupled with supercomputingpower has allowed a team of three computing scientists to solve theBoolean Pythagorean Triples Problem, a long-standing open question inRamsey Theory: Can the set \(\{1, 2,...\}\) of natural numbers bedivided into two parts with no part containing a triple \((a, b, c)\)such that \(a^2 + b^2 = c^2\)? Heule, Kullmann & Marek 2016 provedthat this cannot be done by showing that the set \(\{1, 2, \ldots,n\}\) can be so partitioned for \(n = 7824\) but that this isimpossible for \(n \ge 7825\). Expressing this deceptively simplequestion as a SAT problem required close to 38,000 clauses and 13,000variables with about half of these going to represent that the problemis satisfiable when n \(= 7824\) and the other half to represent thatit is not when n \(= 7825\); of the two, proving the latter was farmore challenging since it demanded a proof of unsatisfiability, i.e.that no such partition exists. A naïve brute-force approachconsidering all \(2^{7825}\) possible two-part partitions was clearlyout of the question and the problem was attacked by using“clever” algorithms within a multi-stage SAT-basedframework for solving hard problems in combinatorics, consisting offive phases:Encode (encoding the problem as SAT formulas),Transform (optimizing the encoding using clause eliminationand symmetry breaking techniques),Split (dividing theproblem effectively into subproblems using splitting heuristics),Solve (searching for satisfying assignments or their lackthereof using fast processing), andValidate (validating theresults of the earlier phases). Of special importance was theapplication ofcube-and-conquer, a hybrid SATstrategy particularly effective for hard combinatorial problems. Thestrategy combineslook-ahead withconflict-driven clause-learning \((\mathbf{CDCL})\),with the former aiming to construct small binary search trees usingglobal heuristics and the latter aiming to find short refutationsusing local heuristics.

After splitting the problem into \(10^6\) hard subproblems (known as“cubes”), these were handed down to 800 cores working inparallel on aStampede supercomputer which, after 2 days offurther splitting and CDCL clause-crunching, settled the question anddelivered a 200-terabyte proof validating the work. After deservedlycelebrating this significant accomplishment of automated reasoning,and after entertaining all the new applications that the enhanced SATmethod would afford (particularly in the areas of hardware andsoftware verification), we should then ask some questions that are ofespecial importance to mathematicians: Is there a more insightful wayto establish this result that would involve more traditional andintellectually satisfying mathematical proof methods? Or, as far asincreasing our understanding of a given field (combinatorics in thiscase), what is the value of settling a question when no human caninspect the proof and hence get no insight from it? Even the teamresponsible for the result admits that “the proofs ofunsatisfiability coming from SAT solvers are, from a human point ofview, a giant heap of random information (no direct understanding isinvolved)”. The conjecture has been settled but we basicallyhave no underlying idea what makes 7825 so special. Perhaps the realvalue to be drawn from these considerations is that they lead us tothink about the deeper question: What is it about the structure of aspecific problem that makes it amenable to standard mathematicaltreatment as opposed to requiring a mindless brute-force approach?While this question is being contemplated, SAT may provide the bestline of attack on certain mathematical problems.

The DPLL search procedure has been extended to quantified logic. MACEis a popular program based on the DPLL algorithm that searches forfinite models of first-order formulas with equality. As an example(McCune 2001), to show that not all groups are commutative one candirect MACE to look for a model of the group axioms that alsofalsifies the commutation law or, equivalently, to look for a modelof:

MACE finds a six-element model of these axioms, where \(\cdot\) isdefined as:

and where \(i\) are defined as:

This example also illustrates, once again, the benefits of using anautomated deduction system: How long would have taken the humanresearcher to come up with the above or a similar model? For morechallenging problems, the program is being used as a practicalcomplement to the resolution-based theorem prover Prover9 (formerlyOtter), with Prover9 searching for proofs and MACE jointly looking for(counter) models. To find such models, MACE converts the first-orderproblem into a set of "flattened" clauses which, for increasing modelsizes, are instantiated into propositional clauses and solved as a SATproblem. The method has been implemented in other automated reasoningsystems as well, most notably in the Paradox model finder where theMACE-style approach has been enhanced by four additional techniquesresulting in some significant efficiency improvements (Claessen &Sörensson 2003): term definitions (to reduce the number ofvariables in flattened clauses), static symmetric reduction (to reducethe number of isomorphic models), sort inference (to apply symmetricreduction at a finer level) and incremental SAT (to reuse searchinformation between consecutive model sizes). The strategy of pairingthe complementary capabilities of separate automated reasoning systemshas been applied to higher-order logic too as exemplified by Nitpick,a counterexample generator for Isabelle/HOL (Blanchette & Nipkow2010). Brown 2013 describes a theorem proving procedure forhigher-order logic that uses SAT-solving to do most of the work; theprocedure is a complete, cut-free, ground refutation calculus thatincorporates restrictions on instantiations and has been implementedin the Satallax theorem prover (Brown 2012).

An approach of great interest at solving SAT problems in first-orderlogic isSatisfiability Modulo Theory\((\mathbf{SMT})\) where the interpretation of symbols in theproblem’s formulation is constrained by abackgroundtheory. For example, in linear arithmetic the functionsymbols are restricted to + and \(-\). As another example, in theextensional theory of arrays (McCarthy 1962) the array functionread\((a, i)\) returns the value of the array \(a\) at index\(i\), andwrite\((a, i, x)\) returns the array identical to\(a\) but where the value of \(a\) at \(i\) is \(x\). Moreformally,

(read-write axiom 1)

\(\forall a : \textit{Array} . \forall i,j : \textit{Index} .\forall x : \textit{Value} . i = j\ \rightarrow \)\(\textit{read}(write(a, i, x), j) = x\)

(read-write axiom 2)

\(\forall a : \textit{Array} . \forall i,j : \textit{Index} .\forall x : Value . i \ne j\ \rightarrow\)\(\textit{read}(\textit{write}(a, i, x), j) = \textit{read}(a,j)\)

(extensionality)

\(\forall a,b : \textit{Array} . \forall i : \textit{Index} . a =b\ \rightarrow\) \(\textit{read}(a, i) = \textit{read}(b, i)\)

In the context of these axioms, an SMT solver would attempt toestablish the satisfiability (or, dually, the validity) of a givenfirst-order formula, or thousands of formulas for that matter, suchas

(Ganzingeret al. 2004) discusses an approach to SMT called\(\mathbf{DPLL}(\mathbf{T})\) consisting of a general DPLL(X) enginethat works in conjunction with a solverSolver\(_T\) forbackground theory \(T\). Bofillet al. (2008) present theapproach in the setting of the theory of arrays, where the DPLL engineis responsible for enumerating propositional models for the givenformula whereasSolver\(_T\) checks whether these models areconsistent with the theory of arrays. Their approach is sound andcomplete, and can be smoothly extended to multidimensional arrays.

SMT is particularly successful in verification applications, mostnotably software verification. Having improved the efficiency of SATsolvers with SMT, the effort is now on designing more efficient SMTsolvers (de Moura 2007). There is also the need to conduct acomprehensive comparison and potential consolidation of the techniquesoffered by the different SMT-based verification approaches, includingbounded model checking, k-induction, predicate abstraction, and lazyabstraction with interpolants (Beyer, Dangl & Wendler 2018 and2021).

4.3 Deductive Computer Algebra

To prove automatically even the simplest mathematical facts requires asignificant amount of domain knowledge. As a rule, automated theoremprovers lack such rich knowledge and attempt to construct proofs fromfirst principles by the application of elementary deduction rules.This approach results in very lengthy proofs (assuming a proof isfound) with each step being justified at a most basic logical level.Larger inference steps and a significant improvement in mathematicalreasoning capability can be obtained, however, by having a theoremprover interact with a computer algebra system, also known as asymbolic computation system. Acomputer algebrasystem is a computer program that assists the user with thesymbolic manipulation and numeric evaluation of mathematicalexpressions. For example, when asked to compute the improperintegral

a competent computer algebra system would quickly reply with theanswer

Essentially, the computer algebra system operates by taking the inputexpression entered by the user and successively applies to it a seriesof transformation rules until the result no longer changes (seethe section on Term Rewriting for more details). These transformation rules encode a significantamount of domain (mathematical) knowledge making symbolic systemspowerful tools in the hands of applied mathematicians, scientists, andengineers trying to attack problems in a wide variety of fieldsranging from calculus and the solving of equations to combinatoricsand number theory.

Problem solving in mathematics involves the interplay of deduction andcalculation, with decision procedures being a reminder of the fuzzydivision between the two; hence, the integration of deductive andsymbolic systems, which we coin here asDeductive ComputerAlgebra (DCA), is bound to be a fruitful combination.Analytica (Bauer, Clarke & Zhao 1998) is a theorem prover built ontop of Mathematica, a powerful and popular computer algebra system.Besides supplying the deductive engine, Analytica also extendsMathematica’s capabilities by defining a number of rewriterules—more precisely, identities about summations andinequalities—that are missing in the system, as well asproviding an implementation of Gosper’s algorithm for findingclosed forms of indefinite hypergeometric summations. Equipped withthis extended knowledge, Analytica can prove semi-automatically somenontrivial theorems from real analysis, including a series of lemmasdirectly leading to a proof of the Bernstein Approximation Theorem.Here is the statement of the theorem simply to give the reader a senseof the level of the mathematical richness we are dealing with:

Bernstein Approximation Theorem.
Let \(\text{I} = [0, 1]\) be the closed unit interval, \(f\) a realcontinuous function on I, and \(B_n (x,f)\) thenth Bernsteinpolynomial for \(f\) defined as \[B_n(x, f)= \sum_{k=0}^n \binom{n}{k} f(k/n)x^k(1-x)^{n-k}\] Then, on the interval I,the sequence of Bernstein polynomials for \(f\) converges uniformly to\(f\).

To be frank, the program is supplied with key information to establishthe lemmas that lead to this theorem but the amount and type ofdeductive work done by the program is certainly nontrivial. (Clarke& Zhao 1994) provides examples of fully automated proofs usingproblems in Chapter 2 ofRamanujan’s Notebooks (Berndt1985) including the following example that the reader is invited totry. Show that:

where \(A_0 =1\), \(A_{n+1}=3A_n +1\) and \(\phi(x,n)\) isRamanujan’s abbreviation for

Analytica’s proof of this identity proceeds by simplifying boththe left- and right-hand sides of the equality and showing that bothsides reduce to the same expression, \(-H_n +\) \(H_{A_r}\). Thesimplification uses the added summation identities mentioned before aswell as some elementary properties of the harmonic numbers,

The resulting proof has 28 steps (some of which are nontrivial) takingabout 2 minutes to find.

Kerber, Kohlhase & Sorge 1998 use the \(\Omega\)mega planningsystem as the overall way to integrate theorem proving and symboliccomputation. In Harrison & Théry 1998, we find an exampleof the integration of a higher-order logic theorem proving system(HOL) with a computer algebra system (Maple).

Their great power notwithstanding, symbolic algebra systems do notenforce the same level of rigor and formality that is the essence ofautomated deduction systems. In fact, the mathematical semantics ofsome of the knowledge rules in most algebra systems is not entirelyclear and are, in cases, logically unsound (Harrison &Théry 1998). The main reason for this is an over-aggressivenessto provide the user with an answer in a timely fashion at whatevercost, bypassing the checking of required assumptions even if it meanssacrificing the soundness of the calculation. (This is stronglyreminiscent of most Prolog implementations that bypass the so-called“occurs-check” also abandoning logical soundness in thename of efficiency.) This serious problem opens the opportunity for adeduction system to provide a service to the computer algebra system:Use its deductive capabilities to verify that the computeralgebra’s computational steps meet the required assumptions.There is a catch in this, however: For sufficiently large calculationsteps, verifying is tantamount to proving and, to check these steps,the deduction system may well need the assistance of the very samesystem that is in need of verification! The solution to the soundnessproblem may then well require an extensive modification of the chosensymbolic algebra system to make it sound; an alternative approach isto develop a new system, entirely from scratch, in conjunction withthe development of the automated theorem prover. In either case, theresulting combined deductive computer algebra system should display amuch improved ability for automated mathematical reasoning.

4.4 Formal Verification of Hardware

Automated reasoning has reached the level of maturity where theoremproving systems and techniques are being used for industrial-strengthapplications. One such application area is the formal verification ofhardware and software systems. The cost of defects in hardware caneasily run into the millions. In 1994, the Pentium processor wasshipped with a defect in its floating-point unit and the subsequentoffer by Intel to replace the flawed chip (which was taken up only bya small fraction of all Pentium owners) cost the company close to $500million. To guard against situations like this, the practice oftesting chip designs is now considered insufficient and more formalmethods of verification have not only gained large attention in themicroprocessor industry but have become a necessity. The idea behindformal verification is to rigorously prove with mathematical certaintythat the system functions as specified. Common applications tohardware design include formally establish that the system functionscorrectly on all inputs, or that two different circuits arefunctionally equivalent.

Depending on the task at hand, one can draw from a number of automatedformal verification techniques, including SAT solvers in propositionallogic, symbolic simulation using binary decision diagrams (BDDs),model checking in temporal logic, or conducting proofs in higher-orderlogic. In the latter case, using an automated theorem prover likeHOL—see Section 3.1—has shown to be invaluable inpractice. Proof construction in a system like HOL proceedssemi-automatically with the user providing a fair amount of guidanceas to how the proof should proceed: The user tries to find a proofwhile being assisted by the theorem prover which, on request, caneither automatically fill in a proof segment or verify proof stepsgiven to it. Although some of the techniques mentioned above providedecision procedures which higher-order logic lacks, higher-order logichas the advantage of being very expressive. The tradeoff is justifiedsince proving facts aboutfloating-point arithmeticrequires the formalization of a large body of real analysis, includingmany elementary statements such as:

This statement from Harrison 2000 written in HOL says that if afunction \(f\) is differentiable with derivative \(f'\) in an interval\([a, b]\) then a sufficient condition for \(f(x) \le K\) throughoutthe interval is that \(f(x) \le K\) at the endpoints \(a, b\) and atall points of zero derivative. The result is used to determine errorbounds when approximating transcendental functions by truncated powerseries. Conducting proofs in such a “painstakingly foundationalsystem” (Harrison 2006) has some significant benefits. First,one achieves a high degree of assurance that the proofs are validsince (admitedly lengthy) they are composed of small error-freedeductive steps. Second, the formalization of these elementarystatements and intermediate results can be reused in other tasks orprojects. For example, a library of formal statements and provenresults in floating-point division can be reused when proving otherresults of floating-point algorithms for square roots ortranscendental functions. To further illustrate, different versions ofthe square root algorithm for the Intel Itanium share manysimilarities and the proof of correctness for one version of thealgorithm can be carried over to another version after minor tweakingof the proof. A third benefit of using a prover like HOL is, ofcourse, that such lengthy proofs are carried out mechanically and aredeductively certain; the likelihood of introducing a human error ifthey were carried out manually would be just as certain.

Formal verification frameworks have become an indispensable part ofthe microprocessor design process, as exemplified by the use of theACL2 theorem prover at Centaur Technology (Hunt, Kaufmann, Moore andSlobodova 2017). ACL2 is used as an integrated programming and proofenvironment in the formal specification of microprocessors, formalmodels of hardware design and their associated proofs, and to supportthe design of other formal analysis tools. Uses of ACL2 to provegroup-theoretic properties of elliptic curves (Russinoff 2017) echothe aforementioned work of Harrison 2000 within abstract mathematicaldomains in order to serve the needs of wordly microprocessor design.

4.5 Formal Verification of Software

Society is becoming increasingly dependent on software systems forcritical services such as safety and security. Serious adverse effectsof malfunctioning software include loss of human life, threats tosecurity, unauthorized access to sensitive information, largefinancial losses, denial of critical services, and risk to safety. Oneway to increase the quality of critical software is to supplementtraditional methods of testing and validation with techniques offormal verification. The basic approach to formal verification is togenerate a number of conditions that the software must meet and toverify—establish—them by mathematical proof. As withhardware, automated formal verification (simply formal verification,hereafter) is concerned with discharging these proof obligations usingan automated theorem prover.

The formal verification ofsecurity protocols is analmost ideal application of automated theorem proving in industry.Security protocols are small distributed programs aimed at ensuringthat transactions take place securely over public networks. Thespecification of a security protocol is relatively small and welldefined but its verification is certainly non-trivial. We have alreadymentioned in a previous section the use of SAT-based theorem proversin the verification of the U.S Data Encryption Standard (DES). Asanother example, the Mondex “electronic purse” is a smartcard electronic cash system that was originally developed by NationalWestminster Bank and subsequently sold to MasterCard International.Schmitt & Tonin 2007 describe a Java Card implementation of theMondex protocol for which the security properties were reformulated inthe Java Modeling Language (JML) following closely the original Zspecification. Proof of correctness was conducted using the KeY tool(Beckert, Hanle & Schmitt 2007), an interactive theorem provingenvironment for first-order dynamic logic that allows the user toprove properties of imperative and object-oriented sequentialprograms. This application of automated reasoning demonstrates, in thewords of the authors, that “it is possible to bridge the gapbetween specification and implementation ensuring a fully verifiedresult”.

Denney, Fischer & Schumann 2004 describe a system to automate thecertification of safety properties of data-analysisaerospacesoftware at NASA. Using Hoare-style program verificationtechniques, their system generates proof obligations that are thenhandled by an automated theorem prover. The process is not fullyautomated, however, since many of the obligations must be simplifiedfirst in order to improve the ability of the theorem prover to solvethe proof tasks. For example, one such class of obligations makes astatement about a matrix, \(r\), that needs to remain symmetric afterupdates along its diagonal have been made, and has the form:

Original form:
\(\textit{symm}(r)\rightarrow\textit{symm}(\textit{diag-updates}(r))\)

Simplified form (when \(r\) is 2x2):

Even after the simplification, current theorem provers find the prooftask challenging. The task becomes intractable for larger matrices andnumber of updates (e.g. a \(6\times 6\) matrix with 36 updates) andfurther preprocessing and simplification on the obligation is requiredbefore the task eventually falls within the reach of state-of-arttheorem provers. But it is worth remarking that proofs are foundwithout using any specific features or configuration parameters of thetheorem provers which would improve their chances at completing theproofs. This is important since the everyday application of theoremprovers in industry cannot presuppose such deep knowledge of theprover from their users. The formal verification of software remains ademanding task but it is difficult to see how the certification ofproperties could happen without the assistance of automated deductionwhen one faces the humanly impossible task of establishing thousandsof such obligations.

In the field ofnuclear engineering, techniques ofautomated reasoning are deemed mature enough to assist in the formalverification of the safety-critical software responsible forcontrolling a nuclear power plant’s reactor prevention systems(RPS). The RPS component of the digital control system of the APR-1400nuclear reactor is specified using NuSCR, a formal specificationlanguage customized for nuclear applications (Yoo, Jee & Cha2009). Model checking in computation tree logic is used to check thespecifications for completeness and consistency. After this, nuclearengineers generate function block designs via a process of automaticsynthesis and formally verify the designs also using techniques ofmodel checking in linear temporal logic; the techniques are also usedto verify the equivalence of the multiple revisions and releases ofthe design. These model-checking tools were implemented to make theiruse as easy and intuitive as possible, in a way that did not require adeep knowledge of the techniques, and used notations familiar tonuclear engineers. The use of automated reasoning tools not only helpsthe design engineers to establish the desired results but it alsoraises the confidence of the government’s regulatory personnelthat need to approve the RPS software before the reactor can becertified for operation.

Quantum computing is an emerging field at theintersection of physics and computer science. The field is expected tobring very significant practical applications and, given the nature ofthe quantum world, we can rest assured there will be no shortage ofphilosophical implications. These applications require a firmfoundation, including the formalization and verification of quantumalgorithms and results in quantum information theory. Aiming to thisworthwhile objective, a number of results have already been formalizedin Isabelle/HOL and added to its library so they can be made availablefor further work. After formalizing a number of concepts in quantumcomputing such as qubits, quantum states, quantum gates, entanglement,measurement, matrix representation of quantum circuits, and others,the work proceeds to the formalization of theorems and algorithms(Bordg, Lachnitt & He 2021), including:

• the no-clone theorem, which states that it is impossible to makean exact copy of an unknown quantum state (Wooters & Zurek 1982,Dieks 1982);
• the quantum teleportation protocol, whose formalization had beendone previously in the Coq system (Boender, Kammüller &Nagarajan 2015) but now it is part of Isabelle’s library aswell; the protocol allows the transmission of an unknown quantum statein the absence of a quantum channel using only an entangled pair and aclassical channel;
• the verification of Deutsch’s algorithm and its generalizedversion, the Deutsch-Jozsa’s algorithm (Deutsch 1985). Deutschwas the first to demonstrate that a quantum computer could perform atask faster than any von-Neumann—classical—computer; and,
• a number of results in quantum game theory such as the quantumprisoner’s dilemma, i.e. the quantum version of the classicaldilemma, and the unfair quantum prisoner’s dilemma, where one ofthe prisoners abides by the laws of classical physics while the otherhas the quantum advantage (Eisert, Wilkens & Lewenstein 1999).

Of notable mention is the fact that the formalization of the unfairquantum prisoner’s dilemma into Isabelle/HOL uncovered a flaw inthe original “paper-and-pencil” publication and which hadgone undetected for many years. Under the more formal and strictframework that Isabelle/HOL demands, the so-called quantum“miracle move” (as defined in Eisert, Wilkens &Lewenstein 1999) was found to be of no advantage over a classicalstrategy. This error has now been rectified (Eisert, Wilkens &Lewenstein 2020) thus re-establishing the advantage of a quantumstrategy . Further use of Isabelle/HOL in quantum computing includesthe verification of quantum cryptographic protocols and the additionto Isabelle’s library the formalization of the quantum Fouriertransform which will pave the way for more advanced quantumalgorithms.

4.6 Logic and Philosophy

In the spirit of Wos, Overbeek, Lusk & Boyle 1992, we pose thequestion: What do the following statements about different systems offormal logic and exact philosophy have in common?

• The implicational fragments of the modal logics S4 and S5 havebeen studied extensively over the years. Posed as an open question, itwas eventually shown that there is a single axiom for implicational S4as well as several new shortest axioms for implicational S5 (Ernst,Fitelson, Harris & Wos 2002).
• The \(L\) combinator is defined as \((Lx)y = x(yy)\). Although itwas known that the \(L\)-based combinator \(E_{12} =((L(LL))(L(LL)))((L(LL))(L(LL)))\) satisfies \(E_{12}E_{12} = E_{12}\)the question remained whether a shorter \(L\)-based combinatorsatisfying this property existed. (Glickfeld & Overbeek 1986)showed this to be the case with \(E_8 = ((LL)(L(LL)))(L(LL))\).
• Thirteen shortest single axioms of length eleven for classicalequivalence had been discovered, and \(XCB= e(x, e(e(e(x, y), e(z,y)), z))\) was the only remaining formula of that length whose statuswas undetermined—was it an axiom? For a quarter of a centurythis question remained open despite intense study by variousresearchers. It was finally settled that \(XCB\) is indeed such asingle axiom, thus ending the search for shortest single axioms forthe equivalential calculus (Wos, Ulrich & Fitelson 2002).
• Saint Anselm of Canterbury offered in hisProslogium afamous argument for the existence of God. But, quite recently, asimpler proof has been discovered in the sense that it is shorter anduses fewer assumptions (Oppenheimer & Zalta 2011). In the sametradition, Gödel produced a proof of God’s existence but(Benzmüller & Paleo 2014) have recently proved the sameresult using a weaker logic system while simultaneously addressing amajor criticism of Gödel’s proof.
• In the axioms defining a Robbins algebra, the Huntington’sequation \(-(-(x + y) + -(x + -y)) = x\) can be replaced by a simplerone, namely the Robbins equation \(-(-x + y) + -(-x + -y) = x\). Thisconjecture went unproved for more than 50 years resisting the attacksof many logicians including Tarski until it was eventually proved in(McCune 1997).

We ask again, what do these results have in common? The answer is thateach has been proved with the help of an automated reasoning program.Having disclosed the answer to this question prompts a new one: Howmuch longer would have taken to settle these open problems without theapplication of such an automated reasoning tool?

Modal logic

The strict implicational fragments of the logical systems S4 and S5 ofmodal logic are known as C4 and C5, respectively, andtheir Hilbert-style axiomatizations presuppose condensed detachment astheir sole rule of inference. With insight from Kripke’s work,Anderson & Belnap (1962) published the first axiomatization of C4using the following 3-axiom basis, where the Polish notation‘Cpq’ stands for ‘\(p \rightarrowq\)’.

(1)

\(Cpp \quad CCpqCrCpq \quad CCpCqrCCpqCpr\)

A question was posed sometime after: Is there a shorter suchaxiomatization for C4, using a 2-axiom basis or even a single axiom?Using the automated reasoning program Otter, the authors Ernst,Fitelson, Harris & Wos (2001) settled both questions in theaffirmative. In fact, several 2-axiom bases were discovered of whichthe following turned out to be shortest:

(2)

\(CpCqq \quad CCPCqrCCpqCsCpr \)

Further rounds of automated reasoning work were rewarded with thediscovery of a single axiom for C4; the axiom is 21 symbols long andit was also proved that it is the shortest such axiom:

(3)

\(CCpCCqCrrCpsCCstCuCpt\)

To show that each of (2) and (3) is necessary and sufficient for (1),a circle of proofs was produced using the automated reasoning tool:(1) \(\Rightarrow\) (3) \(\Rightarrow\) (2) \(\Rightarrow\) (1). Asfor C5, its axiomatization was originally published in a paper byLemmon, A. Meredith, D. Meredith, Prior & Thomas (1957) givingseveral 4-, 3-, 2- and 1-axiom bases for C5, including the following3-axiom basis:

(4)

\(CqCpp \quad CCpqCCqrCpr \quad CCCCpqrCpqCpq\)

The publication also included the shortest known 2-axiom bases for C5(actually two of them, containing 20 symbols each) but the shortestsingle axiom for C5 was later discovered by (Meredith and Prior 1964)and having 21 symbols:

(5)

\(CCCCCppqrCstCCtqCsCsq\)

Applying automated reasoning strategies again, Ernst, Fitelson, Harris& Wos 2001) discovered several new bases, including the following2-axiom basis of length 18 and six 1-axiom bases matchingMeredith’s length of 21 (only one of these is given below):

(6)

\(Cpp \quad CCpqCCCCqrsrCpr\)

(7)

\(CCCCpqrCCuuqCCqtCsCpt\)

To show that each of (6) and (7) is necessary and sufficient for (4),a circle of proofs was also produced with the theorem prover: (6)\(\Rightarrow\) (4) \(\Rightarrow\) (7) \(\Rightarrow\) (6).

Combinatory logic

A charming foray intocombinatory logic is presentedin Smullyan 1985 and Glickfeld & Overbeek 1986, where we learnabout a certain enchanted forest inhabited by talking birds. Given anybirds \(A\) and \(B\), if the name of bird \(B\) is spoken to bird\(A\) then \(A\) will respond with the name of some bird in theforest, \(AB\), and this response to \(B\) from \(A\) will always bethe same. Here are some definitions about enchanted birds:

\(\mathbf{B1}\)

Amockingbird \(M\)mimics any bird in the sensethat \(M\)’s response to a bird \(x\) is the same as\(x\)’s response to itself, \(Mx = xx\).

\(\mathbf{B2}\)

A bird \(C\)composes birds \(A\) and \(B\) if \(A(Bx) =Cx\), for any bird \(x\). In other words, \(C\)’s response to\(x\) is the same as \(A\)’s response to \(B\)’s responseto \(x\).

\(\mathbf{B3}\)

A bird \(A\) is fond of a bird \(B\) if \(A\)’s response to\(B\) is \(B\); that is, \(AB = B\).

And here are two facts about this enchanted forest:

\(\mathbf{F1}\)

For any birds \(A\) and \(B\) in the forest there is a bird \(C\)that composes them.

\(\mathbf{F2}\)

There is a mockingbird in the forest.

There have been rumors that every bird in the forest is fond of atleast one bird, and also that there is at least one bird that is notfond of any bird. The challenge to the reader now is, of course, tosettle these rumors using only F1 and F2, and the given definitions(B1)–(B3). Glickfeld & Overbeek 1986 do this in mere secondswith an automated reasoning system using paramodulation, demodulationand subsumption. For a more challenging problem, consider theadditional definitions:

\(\mathbf{B4}\)

A bird is egocentric if it is fond of itself: \(EE = E\).

\(\mathbf{B5}\)

A bird \(L\) is a lark if for any birds \(x\) and \(y\) thefollowing holds: \((Lx)y = x(yy)\).

Smullyan challenges us to prove a most surprising thing about larks:Suppose we are not given any other information except that the forestcontains a lark. Then, show that at least one bird in the forest mustbe egocentric! Below we give the salient steps in the proof found bythe automated reasoning system, where ‘\(S(x, y)\)’ standsfor ‘\(xy\)’ and where clauses (2) and (3) are,respectively, the definition of a lark and the denial of the theorem;numbers on the right are applications of paramodulation:

1	(x1 = x1)
2	(S(S(L, x1), x2) = S(x1, S(x2, x2)))
3	-(S(x1, x1) = x1)
6	(S(x1, S(S(L, S(x2, x2)), x2)) = S(S(L,x1), S(x2, x2)))	2 2
8	(S(x1, S(S(x2, x2), S(x2, x2))) =S(S(L, S(L, x1)), x2))	2 2
9	(S(S(S(L, L), x1), x2) = S(S(x1, x1),S(x2, x2)))	2 2
18	-(S(S(L, S(S(L, S(L, L)), x1)), x1) =S(S(L, S(x1,x1)), x1))	6 3 6 9 8 8
19	[]	18 1

Closer inspection of the left and right hand sides of (18) under theapplication of unification revealed the discovery of a \(10-L\) bird,i.e. a 10-symbol bird expressed solely in terms of larks, which was astrong candidate for egocentricity. This discovery was excitingbecause the shortest egocentric \(L\)-bird known to Smullyan was oflength 12. A subsequent run of the automated reasoning system produceda proof of this fact as well as another new significant bird: Apossible egocentric \(8-L\) bird! A few more runs of the systemeventually produced a 22-line proof (with terms with as many as 50symbols, excluding commas and parentheses) of the fact that\(((LL)(L(LL)))(L(LL))\) is indeed egocentric. The natural questionsto ask next are, of course, whether there are other \(8-L\) egocentricbirds and whether there are shorter ones. The reader may want toattempt this with paper and pencil but, given that there are 429 suchbirds, it may be wiser to try it instead (or in conjunction) with anautomated reasoning program; both approaches are explored in Glickfeld& Overbeek 1986. For a more formal, but admittedly less colorful,introduction to combinatory logic and lambda-conversion the reader isreferred to Hindley & Seldin 1986.

Equivalential calculus

Formulas in the classicalequivalential calculus arewritten using sentential variables and a two-place function symbol,\(e\), for equivalence. The calculus has two rules of inference,detachment (modus ponens) and substitution; the rules can be combinedinto the single rule of condensed detachment: Obtain \(t\theta\) from\(e(s,t)\) and \(r\) where \(s\theta = r\theta\) with mgu \(\theta\).The calculus can be axiomatized with the formulas:

We can dispense with reflexivity since it is derivable from the othertwo formulas. This brings the number of axioms down to two and anatural question to ask is whether there is a single axiom for theequivalential calculus. In 1933, Łukasiewicz found three formulasof length eleven that each could act as a single axiom for thecalculus—here’s one of them:\(e(e(x,y),e(e(z,y),e(x,z)))\)—and he also showed that noshorter single axiom existed. Over time, other single axioms also oflength eleven were found and the list kept growing with additions byMeredith, Kalman and Peterson to a total of 14 formulas of which 13were known to be single axioms and one formula with a yet undeterminedstatus: the formula \(XCB= e(x, e(e(e(x, y), e(z, y)), z))\).(Actually, the list grew to 18 formulas but Wos, Winker, Veroff, Smith& Henschen 1983 reduced it to 14.) Resisting the intense study ofvarious researchers, it remained as an open question for many yearswhether the 14th formula, \(XCB\), was a single axiom for theequivalential calculus (Peterson 1977). One way to answer the questionin the affirmative would be to show that at least one of the 13 knownsingle axioms is derivable from \(XCB\) alone; another approach wouldbe to derive from \(XCB\) the 3-axiom set (E1)–(E3). While Wos,Ulrich & Fitelson 2002 take shots at the former, their line ofattack concentrates on the latter with the most challenging task beingthe proving of symmetry. Working with the assistance of a powerfulautomated reasoning program, Otter, they conducted a concerted,persistent and very aggressive assault on the open question. (Theirarticle sometimes reads like a military briefing from the frontlines!) For simpler problems, proofs can be found by the reasoningprogram automatically; deeper and more challenging ones like the oneat hand require the guidance of the user. The relentless applicationof the reasoning tool involved much guidance in the setting of lemmasas targets and the deployment of an arsenal of strategies, includingthe set of support, forward and backward subsumption, lemmaadjunction, formula complexity, hints strategy, ratio strategy, termavoidance, level saturation, and others. After much effort and CPUtime, the open question finally succumbed to the combined effort ofman and machine and a 61-step proof of symmetry was found, followed byone for transitivity after 10 more applications of condenseddetachment. Subsequent runs of the theorem prover using demodulationblocking and the so-called cramming strategy delivered shorter proofs.Here are the last lines of their 25-step proof which in this caseproves transitivity first followed by symmetry:

With an effective methodology and a strategy that included theassistance of an automated reasoning program in a crucial way, thesearch for shortest single axioms for the equivalent calculus came toan end.

Computational metaphysics

Fitelson & Zalta 2007, Oppenheimer & Zalta 2011, and Alama,Oppenheimer, & Zalta 2015 describe several applications ofautomated reasoning incomputational metaphysics. Byrepresenting formal metaphysical claims as axioms and premises in anautomated reasoning environment using programs like Prover9, Mace4,the E-prover system and Paradox, the logical status of metaphysicalarguments is investigated. After the suitable formalization of axiomsand premises, the model finder program Mace4 is used to help verifytheir consistency. Then, using Prover9, proofs are automaticallygenerated for a number of theorems of the Theory of Plato’sForms, twenty five fundamental theorems of the Theory of PossibleWorlds, the theorems described in Leibniz’s unpublished paper of1690 and in his modal metaphysics, and a fully automated constructionof Saint Anselm’s Ontological Argument. In the latterapplication, Saint Anselm is understood in Oppenheimer & Zalta2011 as having found a way of inferring God’s existence from Hismere being as opposed to inferring God’s actuality from His merepossibility. This allows for a formalization that is free of modaloperators, involving an underlying logic of descriptions, threenon-logical premises, and a definition of God. Here are two keydefinitions in the formalization, as inputted into Prover9, thathelped express the concept of God:

Definition of none_greater:

all x (Object(x) -> (Ex1(none_greater,x)<->

(Ex1(conceivable,x) &

-(exists y (Object(y) &Ex2(greater_than,y,x) &

Ex1(conceivable,y)))))).

Definition of God:

Is_the(g,none_greater).

Part of the challenge when representing in Prover9 these and otherstatements from axiomatic metaphysics was to circumvent some of theprover’s linguistic limitations. For example, Prover9 does nothave definite descriptions so statements of this kind as well assecond-order concepts had to be expressed in terms of Prover9’sexisting first-order logic. But the return is worth the investmentsince Prover9 not only delivered a proof ofEx1(e,g)—thereis one and only oneGod—but does so with an added bonus. A close inspection of theoutput provides yet another example of an automated theorem prover"outreasoning" its users, revealing that some of the logical machineryis actually redundant: The proof can be constructed only using two ofthe logical theorems of the theory of descriptions (called "Theorem 2"and "Theorem 3" in their article), one of the non-logical premises(called "Premise 2"), and the definition of God. We cannot help but toinclude here Prover9’s shorter proof, written in the moreelegant notation of standard logic (from Oppenheimer & Zalta2011):

In the same tradition as St. Anselm’s, Gödel also providedan ontological proof of God’s existence (Gödel 1970, Scott1972). An important difference between the two is Gödel’suse of modal operators to represent metaphysical possibility andnecessity and, of course, his use of symbolic logic for addedreasoning precision. In his proof, Gödel begins by framing theconcept of “positive property” using two axioms, and heintroduces a definition stating that “A God-like being possessesall positive properties”. This is enough logical machinery toprove as a theorem the possibility of God’s existence,\(\Diamond \exists xG(x)\); three more axioms and two additionaldefinitions allow Gödel to further his proof to establish notonly that God exists, \(\exists xG(x)\), but that this is so bynecessity, \(\Box \exists xG(x)\). Gödel’s proof is in theformalism of higher-order modal logic (HOML) using modal operators andquantification over properties. Gödel never published his proofbut he shared it with Dana Scott who produced the version presentedbelow, which is taken from (Benzmüller & Paleo 2014) alongwith its English annotation to aid the reader with its intendedinterpretation:

Axiom A1

\(\forall \varphi[P({\sim}\varphi) \equiv{\sim}P(\varphi)]\)
  Either a property or its negation is positive, but notboth)

Axiom A2

\(\forall \varphi \forall \psi[(P(\varphi) \wedge \Box \forallx[\varphi(x) \rightarrow \psi(x)]) \supset P(\psi)]\)
  A property necessarily implied by a positive propertyis positive

Theorem T1

\(\forall \varphi[P(\varphi) \supset \Diamond \exists x\varphi(x)]\)
  Positive properties are possibly exemplified

Definition D1

\(G(x) \equiv \forall \varphi[P(\varphi) \supset \varphi(x)]\)
  A God-like being possesses all positiveproperties

Axiom A3

\(P(G)\)
  The property of being God-like is positive

Corollary C

\(\Diamond \exists xG(x)\)
  Possibly, God exists

Axiom A4

\(\forall \varphi[P(\varphi) \supset \Box P(\varphi)]\)
  Positive properties are necessarily positive

Definition D2

\(\varphi \ess x \equiv \varphi(x) \wedge \forall \psi(\psi(x)\supset \Box \forall y(\varphi(y) \supset \psi(y)))\)
  An essence of an individual is a property possessed byit and
  necessarily implying any of its properties

Theorem T2

\(\forall x[G(x) \supset G \ess x]\)
  Being God-like is an essence of any God-likebeing

Definition D3

\(NE(x) \equiv \forall \varphi [\varphi \ess x \supset \Box\exists y\varphi(y)]\)
  Necessary existence of an individual is the necessary
   exemplification of all its essences

Axiom A5

\(P(NE)\)
  Necessary existence is a positive property

Theorem T3

\(\Box \exists xG(x)\)
  Necessarily, God exists

The proof has recently been analysed to an unprecedented degree ofdetail and precision by Benzmüller & Paleo 2014 with the helpof automated theorem provers. A major challenge faced by these authorswas the lack of a HOML-based theorem prover that could carry out thework but this was circumvented by embedding the logic into theclassical higher-order logic (HOL) already offered by existing theoremprovers like LEO-II, Satallax and the countermodel finder Nitpick.Details of the syntactic and semantic embedding are given in theirpaper and it consists of encoding HOML formulas as HOL predicates viamappings, expansions, and \(\beta \eta\)-conversions. The mappingassociates HOML types \(\alpha\), terms \(s_{\alpha}\), and logicaloperators \(\theta\) with corresponding HOL “raised” types\(\lceil\alpha\rceil\), type-raised terms \(\lceil s_{\alpha}\rceil\),and type-raised logical operators \(\theta^{\bullet}\). If \(\mu\) and\(\omicron\) are, respectively, the types of individuals and Booleansthen \(\lceil\mu\rceil = \mu\) and \(\lceil\omicron\rceil = \sigma\)where \(\sigma\) is shorthand for \(\iota \rightarrow \omicron\) with\(\iota\) as the type of possible worlds; as for function types,\(\lceil\beta \rightarrow \gamma\rceil =\lceil\beta\rceil\rightarrow\lceil\gamma\rceil\). For type-raisedterms, \(\lceil s_\alpha \rceil\) is defined inductively on thestructure of \(s_\alpha \) as the following example illustrates:

Type-raised logical connectives, \(\theta^{\bullet}\), are definedbelow where \(r\) is a new constant symbol in HOL associated with theaccessibility relation of HOML:

The other connectives can be defined in the usual way. Validity isexpressed as a \(\lambda\)-term, \(\lambda s_{\iota\rightarrow\omicron}\forall w_\iota sw\), that when applied to a term\(s_{\sigma}\) we write as \([s_{\sigma}]\). For example, under theembedding, proving in HOML the possibility of God’s existence,\(\Diamond_{\omicron\rightarrow \omicron}\exists_{(\mu \rightarrow\omicron)\rightarrow \omicron} X_{\mu} . g_{\mu \rightarrow\omicron}X\), is tantamount to proving its validity in HOL:\([\Diamond^{\bullet}_{\sigma \rightarrow\sigma}\exists^{\bullet}_{(\mu \rightarrow \sigma)\rightarrow \sigma}X_{\mu} . g_{\mu \rightarrow \sigma} X]_{\mu \rightarrow\omicron }\).To prove so, the type-raised HOL expression\([\Diamond^{\bullet}\exists^{\bullet}X_{\mu} . g_{\mu\rightarrow\sigma } X]\) is then encoded in the so-called THF0 syntax(Sutcliffe & Benzmüller 2010) prior to being fed, along withthe above set of equality rules, to the provers that were used incompleting the proof:

The proof in Benzmüller & Paleo 2014 is presented here,including the axioms and definitions as well as the derivation of itsfour main results—T1, C, T2, T3—all written in thetype-decorated type-raised higher-order logic notation resulting fromthe embedding. The proof steps are not fully expanded—note thepresence of type-raised connectives—and the inferential movesare not broken down to lower levels of detail. Borrowing a phrase fromBertrand Russell (Urquhart 1994), this was done to spare the reader ofthe “kind of nausea” that the fully detailed automatedproof would cause:

Besides helping in the completion of the proof, the automated theoremprovers were also very instrumental in the finding of some novelresults. First, Gödel’s set of original assumptions wasshown to be inconsistent by LEO-II by proving that self-differencebecomes an essential property of every entity; a re-formulation of thedefinition of essence due to Dana Scott—this involved theaddition of a missing conjunct, \(\varphi X\), in thedefinition—was shown by Nitpick to be consistent. Second, LEO-IIand Satallax managed to prove C, T1 and T2 using only the logic systemK and, moreover, Nitpick found a counter-model for T3 in K thusshowing that more logical power is required to complete the rest ofthe proof. Third, using LEO-II and Satallax, it is shown that thelogic system KB (system K with the Brouwer axiom) is sufficient toestablish the necessity of God’s existence,\(\Box^{\bullet}\exists^{\bullet}X_{\mu} . g_{\mu \rightarrow\sigma}X\), which is a double-win for automated reasoning: a gain in logicaleconomy, and the deeper philosophical result of having effectivelydismissed a major criticism against Gödel’s proof, namelyhis use of the stronger logic system S5. Fourth, the authors alsoprove in KB that:

as well as:

that is, that God is flawless and that monotheism holds, respectively.At this point, it would be fair to say that any of these results wouldbe enough to vindicate the application of automated reasoning in exactphilosophy. Now, for the bad news followed by good news: Fifth, theformula \(s_{\sigma} \supset^{\bullet} \Box^{\bullet}s_{\sigma}\) canalso be formally derived which is unfortunate since it implies thatthere are no contingent truths and that everything is determined, i.e.there is no free will. However, the issue has been addressed byfollow-up work based on Fitting’s and Anderson’s variantsof the ontological argument (Fuenmayor & Benzmüller 2017,Fitting 2002, Anderson 1990).

Abstract object theory (AOT) is a metaphysical theoryof abstract objects (Zalta 1983). Abstract objects are the objectspresupposed by scientific theories: numbers, natural laws, properties,states of affairs, possibilities, etc. AOT draws a fundamentaldistinction between ordinary objects defined as \(O!x =_{df} \DiamondE!x\) and abstract objects defined as \(A!x =_{df}\lnot\Diamond E!x\).AOT also provides two distinctive modes of predication:exemplification \((Fx\), more generally \(Fx_1 ...x_n)\) and encoding\((xF\), ‘\(x\) encodes \(F\)’, and more generally \(x_1...x_n F)\). AOT adds encoding to 2^nd-order S5 quantifiedmodal logic without identity, extended with definite descriptions\(\iota x \phi\), lambda expressions \(\lambda x_1 ...x_n \phi^*\)(where \(\phi^*\) means no encoding of subformulas), and a free logicfor complex terms (Zalta 1983, Zalta 1988). The key axioms of AOT arecomprehension for abstract objects, \[\exists x(A!x \amp \forall F(xF \equiv \phi))\] with no free\(x\)’s in \(\phi\), and classical \(\lambda\)-conversion,\[[\lambda y_1 ...y_n \phi^*]x_1 ...x_n \equiv \phi^* (x_1 /y_1,..., x_n /y_n)\] with no descriptions in \(\phi^*\). These implycomprehension for relations, \[\exists F^n \Box \forall x_1 ...x_n (F^n x_1 ...x_n \equiv \phi^*)\] with no descriptions in\(\phi^*\). Other principles include \[\begin{align}O!x &\rightarrow \Box \lnot\exists FxF\\ \Diamond xF &\rightarrow \Box xF\\ O!x \amp O!y & \rightarrow(x = y \rightarrow \Box \forall F(Fx \equiv Fy))\\ A!x \amp A!y & \rightarrow(x = y \rightarrow \Box \forall F(xF \equiv yF))\end{align}\] and \(\iota x(A!x\amp \forall F(xF \equiv \phi))\) always being well-defined. To give asense of the expressive power and application of AOT, here are someexamples of AOT’s ability to define metaphysical entities asabstract objects and derive interesting results (Zalta 2018):

Plato’s Forms (e.g. triangle)
\(\Phi_T =_{df}\iota x(A!x \amp \forall F(xF \equiv \Box \forall x(Tx\rightarrow Fx)))\)

Leibniz’s Concepts (e.g. Alexander)
\(c_a =_{df}\iota x(A!x \amp \forall F(xF \equiv Fa))\)

Frege Numbers
\(0 =_{df}\iota x(A!x \amp \forall F(xF \equiv\lnot\exists yFy))\)
\(1 =_{df}\iota x(A!x \amp \forall F(xF \equiv \exists y(Fy \amp\forall z(Fz \rightarrow z = y))))\)
etc.

Truth Values
\(\top =_{df}\iota x(A!x \amp \forall F(xF \equiv \exists p(p \amp F =[\lambda y p])))\)
\(\bot =_{df}\iota x(A!x \amp \forall F(xF \equiv \exists p(\lnot p\amp F = [\lambda y p])))\)

Situations and Possible Worlds
\(\textit{Situation}(x) =_{df} \forall F(xF \rightarrow \exists p(F =[\lambda y p]))\)
\(s \vDash p =_{df} s[\lambda y p]\)
\(\textit{PossibleWorld}(x) =_{df} \Diamond \forall p((s \vDash p)\equiv p)\), from which one can derive Leibniz’s Principle that\(p\) is necessary if true in all worlds, \(\vdash \Box p \equiv\forall w(w \vDash p)\), and also Lewis’ Principle that forevery way the world might be, there is a world which is that way,\(\vdash \Diamond p \equiv \exists w(w \vDash p)\)

Theoretical Mathematical Objects (e.g. null set inZF)
\(\varnothing_{ZF} =_{df}\iota x(A!x \amp \forall F(xF \equiv ZF\vDash F\varnothing))\)

AOT is under continuous development and for further details of thetheory the reader is referred to one of its latest formulations (Zalta2022). The computational analysis of AOT was pioneered by Fitelson andZalta (Fitelson & Zalta 2007) by using the first-order systemProver9. Conducting computational investigations of a higher-ordertheory like AOT using a first-order prover has inherent limitationsand it would be preferable to work within the computational frameworkof a higher-order prover. AOT, however, is based on a logicalfoundation that is significantly different from classical higher-orderlogic and, ideally, one would want to work with a theorem prover forAOT itself. The downside to this is, of course, that one would need tobuild such a prover and this is no trivial task. But one can“approximate” such a system to a large extent by buildinginstead ashallow semantic embedding (SSE) of AOTinto an existing higher-order prover like e.g. Isabelle/HOL where theresearcher can faithfully represent AOT’s axioms and deductivesystem (Benzmüller 2019, Kirchner 2021). In this setting,Isabelle/HOL acts as the metalogical framework for the SSE thatprovides the “custom” theorem prover for AOT. But there isalways a trade-off, and building the embedding brings its own set ofchallenges. Key among these is that there are aspects of AOT which canbe easily formulated in relational type theory but present a challengewhen being re-formulated in the underlying functional type theory ofIsabelle/HOL. For example, not every formula in AOT can be convertedto a \(\lambda\)-term unless one is willing to face a contradiction!With some ingenuity, one can use Isabelle/HOL’s functionalcalculus to define some complex types to help build an Aczel model ofAOT, and then interpret those offending \(\lambda\)-expressions interms of the complex types all in the context of a free logic. Thebottom line: Every formula of AOT can then be expressed as a\(\lambda\)-term but not all these terms denote; hence, consistency ispreserved.

Key aspects of the SSE of AOT in Isabelle/HOL include the modelconstruction of the embedding using Aczel models, reproducing thesyntax of AOT, extending Isabelle’s “outer” syntax(to deal with certain challenges of reasoning in AOT), representing anabstract semantics of AOT, specifying the logic of the Hilbert\(\varepsilon\) operator, representing the logic of the actualityoperator, representing hyperintensionality, deriving the axiom systemand deductive system, and other considerations—see Kirchner 2021for details. Salient among these is the use ofabstractionlayers (Kirchner 2017) which play an important role indetermining the derivability of a statement from the deductive systemof the target theory (AOT here). An abstraction layer is constructedby proving that the axioms and deduction rules of AOT are semanticallyvalid in the SSE; after this, all subsequent reasoning (as conductedby e.g. sledgehammer, Isabelle/HOL’s main tool for automatedreasoning) is restricted to rely on the derived axioms and deductionrules themselves and may not refer to the underlying semantics. Thework took about 25,000 lines of Isabelle/HOL: About 5,000 lines tobuild the required model structure and semantics as well as the syntaxrepresentation of AOT, and the remaining 20,000 for the logicreasoning in AOT. Under the embedding, computational explorations ofAOT can be conducted in a more “native” fashion asillustrated below in the 9-line proof in Isabelle/HOL notation that noobject is both ordinary and abstract (Kirchner 2021):

An additional 1,000 lines of such computational derivations lead tothe result that there are distinct abstract objects which cannot bedistinguished by exemplification: \(\exists x\exists y(A!x \amp A!y\amp x \ne y \amp \forall F(Fx \equiv Fy))\). A few more derivationsland a significant novel discovery which provides the analytical meansto determine if a \(\lambda\)-expression denotes in AOT: \([\lambda x\phi]\downarrow \equiv \Box \forall x\forall y(\forall F(Fx \equiv Fy)\rightarrow(\phi \equiv \phi(y/x))\) with \(y\) not free in \(\phi\).And, as a corollary, \([\lambda x \phi]\downarrow \rightarrow \forallx\forall y(\forall F(Fx \equiv Fy) \rightarrow \Box(\phi \equiv\phi(y/x))\) with \(y\) not free in \(\phi\). The proof of the latterin the context of the SSE takes the 20 lines in Isabelle/HOL givenbelow:

After establishing further results about basic logical objects,restricted variables, the extended relation comprehension, andpossible worlds, the computational exploration can then be redirectedto Dedekind-Peano arithmetic where its postulates for natural numbersare formally derived in a system free of mathematical primitivenotions and mathematical axioms—Frege’s Theorem—andthereby supporting the claim that AOT can provide a philosophicallygrounded basis for objects of mathematics. The computational approachin Kirchner 2021 is guided by a proof outline that was previouslygiven in Zalta 1999 but that now, being reconstructed in Isabelle/HOL,produces derivations of the postulates in full detail and formality.

Postulate 1
AOT_theorem "0-n": ❬[ℕ]0 ❭

Postulate 2
AOT_theorem "0-pred":❬ ¬∃n [ℙ]n 0 ❭

Postulate 3
AOT_theorem "no-same-succ":❬ ∀n∀m∀k([ℙ]nk & [ℙ]mk→ n = m) ❭

Postulate 4
AOT_theorem "th-succ":❬ ∀n∃!m [ℙ]nm ❭

Postulate 5
AOT_theorem induction:❬ ∀F([F]0 & ∀n∀m([ℙ]nm →([F]n → [F]m)) → ∀n[F]n) ❭

The computational explorations described above were done using thesecond-order fragment of AOT but the SSE could be extended to the fullhigher-order logic AOT (Kirchner 2021) where it could be applied tothe analysis of theoretical mathematics. It is important to stressthat embedding a target theory within the higher-order logic of anexisting prover results in more than just a formalization of thetheory: The SSE allows for the discovery of new results within thetarget theory, as exemplified above, as well as the study and furtherdevelopment of the target theory itself such as placing the theory onfirmer foundations, e.g. avoiding known paradoxes (Zalta 2018,Kirchner 2021). The computational analysis of AOT described in herecan also be construed as yet another test of the concept of embeddingtheories, simple and complex alike, within the framework of ahigher-order prover. It illustrates the power and convenience of theapproach, and researchers in automated reasoning may want to seriouslyconsider using an SSE in their theorem-proving efforts(Benzmüller 2019).

Leibniz’s dream was to have acharateristicauniversalis andcalculus ratiocinator that would allowus to reason in metaphysics and morals in much the same way as we doin geometry and analysis; that is to say, to settle disputes betweenphilosophers as accountants do: “To take pen in hand, sit downat the abacus and, having called in a friend if they want, say to eachother: Let us calculate!” From the above applications ofautomated reasoning, one would agree with the researchers when theyimply that these results achieve, to some extent, Leibniz’s goalof a computational metaphysics (Fitelson & Zalta 2007,Benzmüller & Paleo 2014).

Procedural epistemology

Work in computational metaphysics has implications in other areas inphilosophy such as e.g. epistemology. An obvious example is ourimproved epistemological standing when errors in our reasoning are(computationally) detected and corrected. Also, proofs produced byautomated reasoning systems can help us better understand complexarguments, and see more quickly the consequences of revising ourtheories by the introduction, or removal, or axioms—a sort of“what-if analysis”. To illustrate, in the desire tosimplify the foundations of AOT, one can attempt the removal ofconstraints in the comprehension principle but it can be shown thatthis move leads to a paradox in a non-trivial way (Kirchner 2021).Finding alternative axiom sets for a given theory can help reduce theepistemological load needed to prove meta-theoretical results such assoundness. In brief, “one of the great benefits of usingcomputational techniques is that enables us to see exactly what thecommitments of our theories are” (Zalta 2018).

As a direct application in epistemology, a nonmonotonic theorem provercan provide the basis for a “computational laboratory” inwhich to explore and experiment with different models of artificialrationality; the theorem prover can be used to equip an artificialrational agent with an inference engine to reason and gain informationabout the world. In suchprocedural epistemology, arational agent is defeasible (i.e. nonmonotonic) in the sense that newreasoning leads to the acceptance of new beliefs but also to theretraction of previously held beliefs in the presence of newinformation. At any given point in time, the agent holds a set ofjustified beliefs but this set is open to revision and is in acontinuous set of flux as further reasoning is conducted. This modelbetter reflects our accepted notion of rationality than a model inwhich all the beliefs are warranted, i.e. beliefs that once areattained are never retracted. Actually, a set of warranted beliefs canbe seen as justified beliefs “in the limit”, that is, asthe ultimate epistemic goal in the agent’s search for trueknowledge about its world. (Pollock 1995) offers the followingdefinition:

A set is defeasible enumerable iff there is an effective computablefunction \(f\) such that for each \(n, f(n)\) is a recursive set andthe following two conditions hold

1.

\((\forall x)(x \in A \rightarrow (\exists n)(\forall m \gt n) x\in f(m))\)

2.

\((\forall x)(x \not\in A \rightarrow (\exists n)(\forall m \gt n)x \not\in f(m))\)

To compare the concepts, if \(A\) is recursively enumerable then thereis a sequence of recursive sets \(A_i\) such that each \(A_i\) is asubset of \(A\) with each \(A_i\) growing monotonically, approaching\(A\) in the limit. But if \(A\) is only defeasibly enumerable thenthe \(A_i\)’s still approach \(A\) in the limit but may not besubsets of \(A\) and approach \(A\) intermittently from above andbelow. The goal of the OSCAR Project (Pollock 1989) is to construct ageneral theory of rationality and implement it in an artificialcomputer-based rational agent. As such, the system uses a defeasibleautomated reasoner that operates according to the maxim that the setof warranted beliefs should be defeasible enumerable. OSCAR has beenin the making for some time and the application of automatednonmonotonic reasoning has also been used to extend its capabilitiesto reason defeasibly about perception and time, causation, anddecision-theoretic planning (Pollock 2006).

4.7 Mathematics

One of the main goals of automated reasoning has been the automationof mathematics. An early attempt at this was Automath (de Bruijn 1968)which was the first computer system used to check the correctness ofproofs and whole books of mathematics, including Landau’sGrundlagen der Analysis (van Benthem Jutting 1977). Automathhas been superseded by more modern and capable systems, most notablyMizar. The Mizar system (Trybulec 1979, Muzalewski 1993) is based onTarski-Grothendieck set theory and, like Automath, consists of aformal language which is used to write mathematical theorems and theirproofs. Once a proof is written in the language, it can be checkedautomatically by Mizar for correctness. Mizar proofs are formal butquite readable, can refer to definitions and previously provedtheorems and, once formally checked, can be added to the growing MizarMathematical Library (MML) (Bancerek & Rudnicki 2003, Bancereket al. 2018). As of June 2018, MML contained about 12,000definitions and 59,000 theorems. The Mizar language is a subset ofstandard English as used in mathematical texts and is highlystructured to ensure the production of rigorous and semanticallyunambiguous texts. Here’s a sample proof in Mizar of theexistence of a rational numberx\(^y\) where \(x\) and \(y\)are irrational:

Examples of proofs that have been checked by Mizar include theHahn-Banach theorem, the Brouwer fixed-point theorem,Kőnig’s lemma, the Jordan curve theorem, andGödel’s completeness theorem. Rudnicki (2004) discusses thechallenges of formalizing Witt’s proof of the Wedderburntheorem:Every finite division ring is commutative. Thetheorem was formulated easily using the existing formalizationsavailable in MML but the proof demanded further entries into thelibrary to formalize notions and facts from algebra, complex numbers,integers, roots of unity, cyclotomic polynomials, and polynomials ingeneral. It took several months of effort to supply the missingmaterial to the MML library but, once in place, the proof wasformalized and checked correct in a matter of days. Clearly, arepository of formalized mathematical facts and definitions is aprerequisite for more advanced applications. The QED Manifesto (Boyeret al. 1994, Wiedijk 2007) has such aim in mind and there ismuch work to do: Mizar has the largest such repository but even after30 years of work “it is minuscule with respect to the body ofestablished mathematics” (Rudnicki 2004). This last remarkshould be construed as a call to increase the effort toward thisimportant aspect in the automation of mathematics.

Mizar’s goal is to assist the practitioner in the formalizationof proofs and to help check their correctness; other systems aim atfinding the proofs themselves. Geometry has been a target of earlyautomated proof-finding efforts. Chou (1987) proves over 500 geometrytheorems using the algebraic approach offered by Wu’s method andthe Gröbner basis method by representing hypotheses andconclusions as polynomial equations. Quaife (1992) provides anotherearly effort to find proofs in first-order mathematics: over 400theorems in Neumann-Bernays-Gödel set theory, over 1,000 theoremsin arithmetic, a number of theorems in Euclidian geometry, andGödel’s incompleteness theorems. The approach is bestdescribed as semi-automatic or “interactive” with the userproviding a significant amount of input to guide the theorem-provingeffort. This is no surprise since, as one applies automated reasoningsystems into richer areas of mathematics, the systems take more on therole of proof assistants than theorem provers. This is because inricher mathematical domains the systems need to reason about theoriesand higher-order objects which in general takes them deeper into theundecidable.Interactive theorem proving is arguablythe “killer” application of automated reasoning inmathematics and much effort is being expended in the building ofincreasingly capable reasoning systems that can act as assistants toprofessional mathematicians. The proof assistant Isabelle/HOL providesthe user with an environment in which to conduct proofs expressed in astructured, yet human-readable, higher-order logic language and whichincorporates a number of facilities that increase the user’sproductivity, automates proof-verification and proof-finding tasks,and provides a modular way for the user to build and manage theoryhierarchies (Ballarin 2014). More recently, using both automated andinteractive theorem proving techniques, Quafie’s work inTarskian geometry has been extended with the proving of additionaltheorems (some of which required Ph.D. level proofs), including fourchallenge problems left unsolved by Quaife, and the derivation ofHilbert’s 1899 axioms for geometry from Tarski’s axioms(Beeson and Wos 2017).

Different proof assistants offer different capabilities measured bytheir power at automating reasoning tasks, supported logic, objecttyping, size of mathematical library, and readability of input andoutput. A “canonical” proof which is not too trivial butnot too complex either can be used as a baseline for systemcomparison, as done in (Wiedijk 2006) where the authors of seventeenreasoning systems are tasked with establishing the irrationality of\(\sqrt{} 2\). The systems discussed are certainly more capable thanthis and some have been used to assist in the formalization of farmore advanced proofs such as Erdös-Selberg’s proof of thePrime Number Theorem (about 30,000 lines in Isabelle), theformalization of the Four Color Theorem (60,000 lines in Coq), and theJordan Curve Theorem (75,000 lines in HOL Light). A milestone ininteractive theorem proving was reached in 2012 when, after six-yearsof effort and using the Coq proof assistant, George Gonthier and histeam completed the formal verification of the 255-page proof of theFeit-Thompson theorem, also known as the Odd Order Theorem, a majorstep in the classification of finite simple groups. Other, morerecent, successes include the resolution of Keller’s conjecture(Brakensieket al. 2022), the formalization of metric spaces(Maggesi 2018), and the formalization and classification of finitefields (Chan and Norrish 2019).

The above notwithstanding, automated reasoning has had a small impacton the practice of doing mathematics and there is a number of reasonsgiven for this. One reason is that automated theorem provers are notsufficiently powerful to attempt the kind of problems mathematicianstypically deal with; that their current power is, at best, at thelevel of first-year undergraduate mathematics and still far fromleading edge mathematical research. While it is true that currentsystems cannot prove completely on their own problems at this level ofdifficulty we should remember that the goal is to build reasoningsystems so that “eventually machines are to be an aid tomathematical research and not a substitute for it” (Wang 1960).With this in mind, and while the automated reasoning communitycontinues to try to meet the grand challenge of building increasinglypowerful theorem provers, mathematicians can draw now some of thebenefits offered by current systems, including assistance incompleting proof gaps or formalizing and checking the correctness ofproposed proofs. Indeed, the latter may be an application that couldhelp address some real issues currently being faced by themathematical community. Consider the announcement by Daniel Goldstonand Cem Yildrim of a proof of the Twin Prime Conjecture where,although experts initially agreed that the proof was correct, aninsurmountable error was found shortly after. Or, think about the caseof Hales’ proof of the Kepler Conjecture which asserts that nopacking of congruent balls in Euclidean 3-space has density greaterthan the face-centered cubic packing. Hales’ proof consists ofabout 300 pages of text and a large number of computer calculations.After four years of hard work, the 12-person panel assigned byAnnals of Mathematics to the task of verifying the proofstill had genuine doubts about its correctness. Thomas Hales, for one,took upon himself to formalize his proof and have it checked by anautomated proof assistant with the aim of convincing others of itscorrectness (Hales 2005b, in Other Internet Resources). His task wasadmittedly heavy but the outcome is potentially very significant toboth the mathematical and automated reasoning communities. All eyeswere on Hales and his formal proof as he announced the completion oftheFlyspeck project (Hales 2014, in Other InternetResources; Hales 2015) having constructed a formal proof of theconjecture using the Isabelle and HOL Light automated proofassistants: “In truth, my motivations for the project are farmore complex than a simple hope of removing residual doubt from theminds of few referees. Indeed, I see formal methods as fundamental tothe long-term growth of mathematics.” (Hales 2006).

Church 1936a, 1936b and Turing 1936 imply the existence of theoremswhose shortest proof is very large, and the proof of the Four ColorTheorem in (Appel & Haken 1977), the Classification of SimpleGroups in (Gorenstein 1982), and the proof of the Kepler Conjecture in(Hales 2005a) may well be just samples of what is yet to come. As(Bundy 2011) puts it: “As important theorems requiring largerand larger proofs emerge, mathematics faces a dilemma: either thesetheorems must be ignored or computers must be used to assist withtheir proofs.”

The above remarks also counter another argument given for not usingautomated theorem provers: Mathematicians enjoy proving theorems, sowhy let machines take away the fun? The answer to this is, of course,that mathematicians can have even more fun by letting the machine dothe more tedious and menial tasks: “It is unworthy of excellentmen to lose hours like slaves in the labour of calculation which couldsafely be relegated to anyone else if machines were used” (G. W.Leibniz,New Essays Concerning Human Understanding). If stillnot convinced, just consider the sobering prospect of having tomanually check the 23,000 inequalities used in Hales’ proof!

Another reason that is given for the weak acceptance of automatedreasoning by the mathematical community is that the programs are notto be trusted since they may contain bugs—softwaredefects—and hence may produce erroneous results. Formallyverifying automated reasoning programs will help ameliorate this,particularly in the case of proof checkers. Proving programs correctis no easy task but the same is true about proving theorems inadvanced mathematics: Gonthier proved correct the programs used in theformalization of his proof of the Four Color Theorem, but he spent farmore effort formalizing all the graph theory that was part of theproof. So ironically enough, it turns out that at least in this case,and surely there are others, “it is actually easier to verifythe correctness of the program than to verify the correctness of thepen-and-paper mathematics” (Wiedijk 2006). For theorem proversand model finders, a complementary strategy would be to verify theprograms’ results as opposed to the programs themselves.Paraphrasing (Slaney 1994): It does not matter to the mathematicianhow many defects a program may have as long as the proof (or model) itoutputs is correct. So, the onus is in the verification of results,whether produced by machine or man, and checking them by independentparties (where of course the effort may well use automated checkers)should increase the confidence on the validity of the proofs.

It is often argued that automated proofs are too long and detailed.That a proof can be expressed in more elementary steps is in principlevery beneficial since this allows a mathematician to request a proofassistant justify its steps in terms of simpler ones. But proofassistants should also allow the opposite, namely to abstract detailand present results and their justifications using the higher-levelconcepts, language, and notation mathematicians are accustomed to.Exploiting the hierarchical structure of proofs as done in (Denney2006) is a step in this direction but more work along these lines isneeded. Having the proof assistant work at the desired level ofgranularity provides more opportunity for insight during the proofdiscovery process. This is an important consideration sincemathematicians are equally interested in gaining understanding fromtheir proofs as in establishing facts—more about this below.

(Bundy 2011) alludes to a deadlock that is preventing the wideradoption of theorem provers by the mathematical community: On the onehand, the mathematicians need to use the proof assistants to build alarge formal library of mathematical results. But, on the other hand,they do not want to use the provers since there is no such library ofpreviously proved results they can build upon. To break the impasse, anumber of applications are proposed of which assisting themathematician in the search of previously proved theorems is ofparticular promise. Indeed, a thoughtful reuse of library results canlead to concise proofs of non-trivial mathematical problems asexemplified in the proving of some fundamental theorems of linearalgebra (Aransay and Divansón 2017) and probability theory(Avigad, Hölzl and Serafin 2017). During its history, mathematicshas accumulated a huge number of theorems and the number ofmathematical results continues to grow dramatically. In 2010,Zentralblatt MATH covered about 120,000 new publications(Wegner 2011). Clearly, no individual researcher can be acquaintedwith all this mathematical knowledge and it will be increasinglydifficult to cope with one’s ever-growing area of specialtyunless assisted with automated theorem-proving tools that can searchin intelligent ways for previously proved results of interest. Analternative approach to this problem is for mathematicians to tap intoeach other’s knowledge as enabled in computational socialsystems likepolymath andmathoverflow. Theintegration of automated reasoning tools into such social systemswould increase the effectiveness of their collective intelligence bysupporting “the combination of precise formal deductions and themore informal loose interaction seen in mathematical practice”(Martin & Pease 2013, in Other Internet Resources).

Due to real pressing needs from industry, some applications ofautomated reasoning in pure and applied mathematics are more ofnecessity than choice. After having worked on the formalization ofsome elementary real analysis to verify hardware-based floating pointtrigonometric functions, (Harrison 2006, Harrison 2000) mentions thefurther need to formalizemore pure mathematics—italicsare his—to extend his formalization to power series fortrigonometric functions and basic theorems about Diophantineapproximations. Harrison finds it surprising that “suchextensive mathematical developments are used simply to verify that afloating point tangent function satisfies a certain error bound”and, from this remark, one would expect there are other industrialapplications that will demand more extensive formalizations.

Albeit not at the rate originally anticipated, automated reasoning isfinding applications in mathematics. Of these, formal verification ofproofs is of special significance since it not only provides a viablemechanism to check proofs that humans alone could not but it also has,as a side effect, the potential to redefine what it would take for aproof to be accepted as such. As the use of automated reasoningassistants becomes more widespread one can envision their usefollowing a certain methodical order: First, automated reasoning toolsare used for theory exploration and discovery. Then, having identifiedsome target problem, the practitioner works interactively with anautomated assistant to find proofs and establish facts. Finally, anautomated proof checker is used to check the correctness of all finalproofs prior to being submitted for publication and being madeavailable to the rest of the mathematical community via the creationof new entries in a repository of formalized mathematics. It is indeeda matter of time before the application of automated proof assistantsbecomes an everyday affair in the life of the mathematician; it is thegrand challenge of the automated reasoning community to make it happensooner than later.

Besides formal verification, orcertification, anotherimportant aspect of a proof is theexplanation it provides;that is, the reasons it gives as to why the given statement isactually true. This, needless to say, is an important source ofinsight and for many mathematicians it may be the single most valuableaspect of a proof as it allows them to gain a better understanding ofthe nature of the statement being established and of the mathematicaltheory and objects involved; moreover, the approach used in the proofhas the potential of being applicable to the proving of othermathematical results. So when it comes to building theorem provers tobe used by the mathematical community, perhaps there should be lessemphasis on the provers as certifiers, i.e. as proof checkers, andplace more emphasis on the provers as proof solvers, i.e. asassistants in helping the mathematician complete proofs and explainthe steps in doing so. Assuming that a prover were to be powerfulenough to successfully attack proofs in the mathematician’s areaof research, it would be very desirable yet admittedly extremelychallenging if the prover were to also use the very same notation,methods, and techniques of proof-solving used by the mathematicianherself. One could safely bet that mathematicians would be morereceptive to this type of human-oriented theorem prover because theprover would work the same way the mathematician does. Moremathematicians may initially approach such a prover simply out ofsheer curiosity; that is, just to see how the prover would go aboutproving a previously established result. This would certainly be ofmuch interest to students of mathematics since they may need to seehow a given problem (say, from their textbook) has been solved and, byinspecting the proof, want to learn how to do it on their own.

Virtually all automated theorem provers nowadays go about buildingtheir proofs in ways far more akin to machines than to humans (e.g.resolution-driven, connection methods). There are some systems that,after establishing a fact, can present the higher-level steps in theproof in a form more amenable to humans and do so by translating themachine-oriented steps into a human-readable format. The approach hasmerit but it has a significant limitation: How deep into the proof canone continue asking for an explanation before the translation breaksdown? An alternative approach could try to address the situation headon: Why not build a system that directly proves theorems the waymathematicians actually do it? This is indeed a very tall order butthe question is not new and it has been taken up in various forms by asmall minority of researchers going back to the early days ofautomated theorem proving, including Bledsoe 1977 (investigations intonon-resolution methods), Boyer and Moore 1979 (induction by recursiveterm rewriting), Bundyet al. 1991 (automated inductivetheorem proving), Clarke and Zhao 1994 (integration of theorem proverswith symbolic algebra systems), Portoraro 1994 (automated advice tostudents building symbolic logic proofs), Portoraro 1998 (strategicproof construction the way teachers of symbolic logic do and teachit), Pelletier 1998 (building proofs in the predicate calculus the wayhumans do it), Beeson 2001 (proof generation using mathematicalmethods), Buchbergeret al. 2016 (computer-assistednatural-style mathematics), and others. More recently, Ganesalingamand Gowers 2017 describes a theorem prover that solves and presentsproofs of elementary problems in metric space theory where theprogram’s approach is hard to distinguish from what amathematician might prove and write. To illustrate, below is theprogram’s proof that the intersection of two open subsets of ametric space is itself open, and it is given as it was both solved andwritten by the program:

Proof. Let \(x\) be an element of \(A\capB\). Then \(x \in A\) and \(x \in B\). Therefore, since \(A\) is open,there exists \(\eta > 0\) such that \(u \in A\) whenever \(d(x, u) \lt\eta\) and since \(B\) is open, there exists \(\theta > 0\) such that\(v \in B\) whenever \(d(x, v) \lt \theta\). We would like to find\(\delta > 0\) s.t. \(y \in A\cap B\) whenever \(d(x, y) \lt \delta\).But \(y \in A\cap B\) if and only if \(y \in A\) and \(y \in B\). Weknow that \(y\cap A\) whenever \(d(x, y) \lt \eta\) and that \(y\capB\) whenever \(d(x, y) \lt \theta\). Assume now that \(d(x, y) \lt\delta\). Then \(d(x, y) \lt \eta\) if \(\delta \le \eta\) and \(d(x,y) \lt \theta\) if \(\delta \le \theta\). We may therefore take\(\delta = \text{min}\{\eta , \theta \}\) and we are done.

Impressive as it may be, the authors acknowledge a number ofshortcomings and many outstanding challenges in the building andpresentation of such proofs even for elementary problems inmathematics, and the reader is referred to their article for details.As we have already mentioned, building increasingly powerful proversthat can attack problems in advanced areas of mathematical researchand doing so in a human-oriented fashion is admittedly extremelychallenging but also, we need to add, a very worthwhile, promising,and rewarding line of research. Embracing this kind of provers bymathematicians will have clear practical applications both in researchand education. There will be philosophical implications too,especially the moment the provers are endowed with the additionalability to ask for assistance when getting stuck in a proof and, whenthis happens, we will be pressed to ask: Who is interacting with whom,the human with the machine or vice versa? The experience ofinteracting with a theorem prover will have been extended to a newrealm, becoming truly two-sided, more intimate and richer, more of acollaboration than an interaction: the dawn ofcollaborative theorem proving.

4.8 Artificial Intelligence

Since its inception, the field of automated theorem proving has hadimportant applications in the larger field of artificial intelligence(AI). Automated deduction is at the heart of AI applications likelogic programming (see Section 4.1 Logic Programming) where computation is equated with deduction; robotics and problemsolving (Green 1969) where the steps to achieve goals are stepsextracted from proofs; deductive databases (Minkeret al.2014) where factual knowledge is expressed as atomic clauses andinference rules, and new facts are inferred by deduction; expertsystems (Giarratano & Riley 2004) where human expertise in a givendomain (e.g. blood infections) is captured as a collection of IF-THENdeduction rules and where conclusions (e.g. diagnoses) are obtained bythe application of the inference rules; and many others. Anapplication of automated reasoning in AI which is bound to have deepphilosophical implications is the increased use of BDI computationallogics for describing the beliefs, desires, and intentions ofintelligent agents and multi-agent systems (Meyer 2014) and, inparticular, endowing future intelligent systems, such asdecision-support systems or robots, with legal and ethical behaviour.Deontic logic can be automated for the task (Furbachet al.2014) but given that there is no agreement on a universal system ofdeontic logic, ethics “code designers” need a way toexperiment with the different deontic systems (i.e., to lay out axiomsand see what conclusions follow from them) to help them identify thedesired ethic code for the specific application at hand;(Benzmülleret al. 2018) discusses an environment forthis. If actual, physical, robots were to be used in theseexperiments, the term “deontic laboratory” would be quitedescriptive albeit somewhat eerie.

Restricting the proof search space has always been a key considerationin the implementation of automated deduction, and traditionalAI-approaches to search have been an integral part of theorem provers.The main idea is to prevent the prover from pursuing unfruitfulreasoning paths. A dual aspect of search is to try to look for apreviously proved result that could be useful in the completion of thecurrent proof. Automatically identifying those results is no easy taskand it becomes less easy as the size of the problem domain, and thenumber of already established results, grows. This is not a happysituation particularly in light of the growing trend to build largelibraries of theorems such as the Mizar Problems for Theorem Proving(MPTP) (Urbanet al. 2010, Bancerek & Rudnicki 2003) orthe Isabelle/HOL mathematical library (Meng & Paulson 2008), sodeveloping techniques for the discovery, evaluation, and selection ofexisting suitable definitions, premises and lemmas in large librariesof formal mathematics as discussed in (Kühlweinet al.2012) is an important line of research.

Among many other methods, and in stark contrast to automated provers,mathematicians combine induction heuristics with deductive techniqueswhen attacking a problem. The former helps them guide theproof-finding effort while the latter allows them to close proof gaps.And of course all this happens in the presence of the very large bodyof knowledge that the human possesses. For an automated prover, theanalogous counterpart to the mathematician’s body of knowledgeis a large library like MPTP. An analogous approach to using inductiveheuristics would be to endow the theorem prover with inductive,data-driven, machine learning abilities. Urban & Vyskocil 2012 runa number of experiments to determine any gains that may result fromsuch an approach. For this, they use MPTP and theorem provers like Eand SPASS enhanced with symbol-based machine learning mechanisms. Adetailed presentation and statistical results can be found in theabove reference but in summary, and quoting the authors, “thisexperiment demonstrates a very real and quite unique benefit of largeformal mathematical libraries for conducting novel integration of AImethods. As the machine learner is trained on previous proofs, itrecommends relevant premises from the large library that (according tothe past experience) should be useful for proving newconjectures.” Urban 2007 discusses MaLARea (a Machine Learnerfor Automated Reasoning), a meta-system that also combines inductiveand deductive reasoning methods. MaLARea is intended to be used inlarge theories, i.e. problems with a large number of symbols,definitions, premises, lemmas, and theorems. The system works incycles where results proved deductively in a given iteration are thenused by the inductive machine-learning component to place restrictionsin the search space for the next theorem-proving cycle. Albeit simplein design, the first version of MaLARea solved 142 problems out of 252in the MPTP Challenge, outperforming the more seasoned provers E (89problems solved) and SPASS (81 problems solved). Machine learningpremise-selection methods trained on the considerable amount ofmathematical knowledge encoded in Flyspeck’s library of proofs,when combined with theorem provers, provides an AI-type system capableof proving a wide range of mathematical conjectures: Almost 40% of the14,185 theorems can be proved automatically without any guidance fromthe user within 30 seconds on a 14-CPU workstation (Kaliszyk &Urban 2014). Machine learning techniques can also be appliedsuccessfully to the problem of selecting good heuristics in thebuilding of first-order proofs (Bridge, Holden & Paulson2014).

The relationship between automated deduction and machine learning isreciprocal and the former has something to offer to the latter too. Tomention one contribution, deep learning has become the technique ofchoice when it comes to applications in image recognition, languageprocessing, and others, and there is theoretical evidence of itssuperiority over shallow learning. Such mathematical proofs can beformalized using theorem-proving systems like e.g. Isabelle/HOL whileat the same time can contribute to the growth of their libraries withformalized results that can be used for further work aimed to securethe foundations of machine learning (Bentkamp, Blanchette & Klakow2019).

Besides using large mathematical libraries, tapping into web-basedsemantic ontologies is another possible source of knowledge. Pease& Sutcliffe 2007 discuss ways for making the SUMO ontologysuitable for first-order theorem proving, and describes work ontranslating SUMO into TPTP. An added benefit of successfully reasoningover large semantic ontologies is that this promotes the applicationof automated reasoning into other fields of science. Tapping into itsfull potential, however, will require a closer alignment of methodsfrom automated reasoning and artificial intelligence.

5. Conclusion

Automated reasoning is a mature yet still growing field that providesa healthy interplay between basic research and application. Automateddeduction is being conducted using a multiplicity of theorem-provingmethods, including resolution, sequent calculi, natural deduction,matrix connection methods, term rewriting, mathematical induction, andothers. These methods are implemented using a variety of logicformalisms such as first-order logic, type theory and higher-orderlogic, clause and Horn logic, non-classical logics, and so on.Automated reasoning programs are being applied to solve a growingnumber of problems in formal logic, mathematics and computer science,logic programming, software and hardware verification, circuit design,exact philosophy, and many others. One of the results of this varietyof formalisms and automated deduction methods has been theproliferation of a large number of theorem proving programs. To testthe capabilities of these different programs, selections of problemshave been proposed against which their performance can be measured(McCharen, Overbeek & Wos 1976, Pelletier 1986). The TPTP(Sutcliffe & Suttner 1998, Sutcliffe 2017) is a library of suchproblems that is updated on a regular basis. There is also acompetition among automated theorem provers held regularly at the CADEconference (Pelletier, Sutcliffe & Suttner 2002; Sutcliffe 2016,in Other Internet Resources); the problems for the competition areselected from the TPTP library and range from problems in clausenormal form (CNF), fist-order form (FOF), typed first-order form(TFF), monomorphic typed higher-order form (TH0), and others. There isa similar library and competition for SMT solvers (Barretetal. 2013).

Initially, computers were used to aid scientists with their complexand often tedious numerical calculations. The power of the machineswas then extended from the numeric into the symbolic domain whereinfinite-precision computations performed by computer algebra programshave become an everyday affair. The goal of automated reasoning hasbeen to further extend the machine’s reach into the realm ofdeduction where they can be used as reasoning assistants in helpingtheir users establish truth through proof.

Bibliography

• Alama, J., P. Oppenheimer, and E. Zalta, 2015, “AutomatingLeibniz’s Theory of Concepts”,CADE 25: Proceedings ofthe 25th International Conference on Automated Deduction,(Lecture Notes in Artificial Intelligence: Volume 9195), A. Felty andA. Middeldorp (eds.), Berlin: Springer, pp. 73–97.
• Anderson, C. A., 1990, “Some Emendations ofGödel’s Ontological Proof”,Faith andPhilosophy, 7(3): 291–303.
• Anderson, A. R. and N. D. Belnap, 1962, “The Pure Calculusof Entailment”,Journal of Symbolic Logic, 27:19–52.
• Andrews, P. B., 1981, “Theorem-Proving via GeneralMatings”,Journal of the Association for ComputingMachinery, 28 (2): 193–214.
• Andrews, P. B., M. Bishop and C. E. Brown, 2006, “TPS: AHybrid Automatic-Interactive System for Developing Proofs”,Journal of Applied Logic, 4: 367–395.
• Andrews, P. B., M. Bishop, S. Issar, D. Nesmith, F. Pfenning andH. Xi, 1996, “TPS: A Theorem-Proving System for Classical TypeTheory”,Journal of Automated Reasoning, 16 (3):321–353.
• Appel, K., and W. Haken, 1977, “Every Planar Map is FourColorable Part I. Discharging”,Illinois Journal ofMathematics, 21: 429–490.
• Aransay, J., J. Divansón, 2017, “A Formalization inHOL of the Fundamental Theorem of Linear Algebra and Its Applicationto the Solution of the Least Squares Problem”,Journal ofAutomated Reasoning, 58 (4): 509–535.
• Avigad, J. and J. Harrison, 2014, “Formally VerifiedMathematics”,Communications of the ACM, 57 (4):66–75.
• Avigad, J., J. Hölzl and L. Serafin, 2017, “A FormallyVerified Proof of the Central Limit Theorem”,Journal ofAutomated Reasoning, 59 (4): 389–423.
• Baader, F. and T. Nipkow, 1998,Term Rewriting and AllThat, Cambridge: Cambridge University Press.
• Bachmair, L. and H. Ganzinger, 1994, “Rewrite-BasedEquational Theorem Proving with Selection and Simplification”,Journal of Logic and Computation, 4 (3): 217–247.
• Ballarin, C., 2014, “Locales: A Module System forMathematical Theories”,Journal of Automated Reasoning,52 (2): 123–153.
• Bancerek, G. and P. Rudnicki, 2003, “Information Retrievalin MML”,Proceedings of the Second International Conferenceon Mathematical Knowledge Management, LNCS 2594, Heidelberg:Springer-Verlag, pp. 119-132
• Bancerek, G., C. Byliński, A. Grabowski, A. Korniłowicz,R. Matuszewski, A. Naumowicz and K. Pąk, 2018, “The Role ofthe Mizar Mathematical Library for Interactive Proof Development inMizar”,Journal of Automated Reasoning (Special Issue:Milestones in Interactive Theorem Proving), 61 (9):9–31.
• Barret C., M. Deters, L. de Moura, A. Oliveras and A. Stump, 2013,“6 Years of SMT-COMP”,Journal of AutomatedReasoning, 50 (3): 243–277.
• Basin, D. A. and T. Walsh, 1996, “A Calculus for andTermination of Rippling”,Journal of AutomatedReasoning, 16 (1–2): 147–180.
• Bauer, A., E. Clarke and X. Zhao, 1998, “Analytica: AnExperiment in Combining Theorem Proving and SymbolicComputation”,Journal of Automated Reasoning, 21:295–325.
• Beckert, B., R. Hanle and P.H. Schmitt (eds.), 2007,“Verification of Object-Oriented Software: The KeYApproach”,Lecture Notes in Artificial Intelligence(Volume 4334), Berlin: Springer-Verlag.
• Beeson M., 2001, “Automatic Derivation of the Irrationalityof e”,Journal of Symbolic Computation, 32 (4):333–349.
• Beeson,M. and L. Wos, 2017, “Finding Proofs in TarskianGeometry”,Journal of Automated Reasoning, 58 (1),181–207.
• Bentkamp, A., J.C. Blanchette and D. Klakow, 2019, “AFormal Proof of the Expressiveness of Deep Learning”,Journal of Automated Reasoning, 63 (2), 347–368.
• Bentkamp, A., J. Blanchette, S. Tourret, P. Vukmirović andU. Waldmann, 2021, “Superposition with Lambdas”,Journal of Automated Reasoning, 65 (7), 893–940.
• Benzmüller, C., 2019, “Universal (Meta-) LogicalReasoning: Recent Successes”,Science of ComputerProgramming, Vol. 172, 48–62.
• Benzmüller, C. and B. W. Paleo, 2014, “AutomatingGödel’s Ontological Proof of God’s Existence withHigher-Order Automated Theorem Provers”,ECAI 2014:Proceedings of the 21st European Conference on ArtificialIntelligence, T. Schaubet al. (eds.), IOS Press, pp.93–98.
• –––, 2015, “Higher-Order Modal Logics:Automation and Applications”,Reasoning Web 2015, LNCS9203, W. Faber and A. Paschke (eds.), pp. 32–74.
• Benzmüller C., X. Parent and L. van der Torre, 2018, “ADeontic Logic Reasoning Infrastructure”,CiE2018:Proceedings of the 14th Conference on Computability in Europe,LNCS 10936, F. Maneaet al. (eds.), pp. 60–69.
• Benzmüller C. and L. C. Paulson, 2013, “QuantifiedMultimodal Logics in Simple Type Theory”,LogicaUniversalis, 7 (1): 7–20.
• Benzmüller, C. and D. S. Scott, 2020, “Automating FreeLogic in HOL, with an Experimental Application in CategoryTheory”,Journal of Automated Reasoning, 64 (1),53–72.
• Benzmüller, C., A. Steen and M. Wisniewski, 2017,“Leo-III version 1.1 (system description)”,Logic forProgramming, Artificial Intelligence, and Reasoning (LPAR)—ShortPapers, T. Eiter, D. Sands, G. Sutcliffe and A. Voronkov (eds.),Kalpa Publications in Computing, Volume 1: 11–26.
• Benzmüller, C., N. Sultana, L. C. Paulson and F. Theiß,2015, “The Higher-Order Prover LEO-II”,Journal ofAutomated Reasoning, 55 (4): 389–404.
• Berndt, B., 1985,Ramanujan’s Notebooks (Part I),Berlin: Springer-Verlag, pp. 25-43.
• Beyer, D., M. Dangl and P. Wendler, 2018, “A Unifying Viewon SMT-Based Software Verification”,Journal of AutomatedReasoning, 60 (3): 299–335.
• Beyer, D., M. Dangl and P. Wendler, 2021, “Correction to: AUnifying View on SMT-Based Software Verification”,Journalof Automated Reasoning, 65 (3): 461.
• Bibel, W., 1981, “On Matrices with Connections”,Journal of the Association of Computing Machinery, 28 (4):633–645.
• Blanchette, J. C., S. Böhme and L. C. Paulson, 2013,“Extending Sledgehammer with SMT Solvers”,Journal ofAutomated Reasoning, 51 (1): 109–128.
• Blanchette, J. C. and T. Nipkow, 2010, “Nitpick: ACounterexample Generator for Higher-Order Logic Based on a RelationalModel Finder”,ITP2010: First International Conference onInteractive Theorem Proving, LNCS 6172, M. Kaufmann and L. C.Paulson (eds.), pp. 131–146.
• Bledsoe, W. W., 1977, “Non-resolution TheoremProving”,Artificial Intelligence, 9: 1–35.
• Bledsoe, W. W. and M. Tyson, 1975, “The UT InteractiveProver”,Memo ATP-17A, Department of Mathematics,University of Texas.
• Boender, J., F. Kammüller and R. Nagarajan, 2015,“Formalization of Quantum Protocols using Coq”, inEPTCS 195: 12th International Workshop on Quantum Physics andLogic (QPL), Chris Heunen, Peter Selinger, and Jamie Vicary(eds.), pp. 71–83. doi:10.4204/EPTCS.195.6
• Bofill, M., R. Nieuwenhuis, A. Oliveras, E. Rodriguez-Carbonelland A. Rubio, 2008, “A Write-Based Solver for SAT Modulo theTheory of Arrays”,Formal Methods in Computer-Aided Design(FMCAD’08), pp. 1–8.
• Bonacina, M. P., 1999, “A Taxonomy of Theorem-ProvingStrategies”,Artificial Intelligence Today, (LectureNotes in Computer Science: Volume 1600), Berlin: Springer-Verlag, pp.43–84.
• Bordg, A., H. Lachnitt and Y. He, 2021, “Certified QuantumComputation in Isabelle/HOL”,Journal of AutomatedReasoning, 65 (5): 691–709.
• Boyer, R. S. and J. S. Moore, 1979,A ComputationalLogic, New York: Academic Press.
• –––, 1997, “Mechanized Formal Reasoningabout Programs and Computing Machines”,Automated Reasoningand Its Applications, R. Veroff (ed.), Cambridge, MA: MIT Press,pp. 147–176.
• Boyer, R. S., M. Kaufmann, and J. S. Moore, 1995, “TheBoyer-Moore Theorem Prover and its Interactive Enhancement”,Computers and Mathematics with Applications, 29:27–62.
• Boyer R. S.,et al., 1994, “The QEDManifesto”,CADE-12: Proceedings of the 12th InternationalConference on Automated Deduction, (Lecture Notes in ArtificialIntelligence: Volume 814), A. Bundy (ed.), Berlin: Springer-Verlag,pp. 238–251.
• Brakensiek, J., M. Heule, J. Mackey and D. Narváez, 2022,“The Resolution of Keller’s Conjecture”,Journalof Automated Reasoning, 66 (3): 277–300.
• Bridge, J. P., S. B. Holden and L.C. Paulson, 2014, “MachineLearning for First-Order Theorem Proving”,Journal ofAutomated Reasoning, 53 (2), 141–172.
• Brown, C. E., 2012, “Satallax: An Automatic Higher-OrderProver”,Automated Reasoning: Proceedings of the 6thInternational Joint Conference on Automated Reasoning (IJCAR2012), LNAI 7364, B. Gramlichet al. (eds.), pp.111–117, Springer-Verlag.
• –––, 2013, “Reducing Higher-Order TheoremProving to a Sequence of SAT Problems”,Journal of AutomatedReasoning, 51 (1): 57–77.
• Buchberger B., T. Jebelean, T. Kutsia, A. Maletzky and W.Windsteiger, 2016, “Theorema 2.0: Computer-AssistedNatural-Style Mathematics”,Journal of FormalizedReasoning, 9 (1): 149–185.
• Bundy, A., 2011, “Automated theorem proving: a practicaltool for the working mathematician?”,Annals of Mathematicsand Artificial Intelligence, 61 (1): 3–14.
• Bundy, A., F. van Harmelen, J. Hesketh and A. Smaill, 1991,“Experiments with Proof Plans for Induction”,Journalof Automated Reasoning, 7 (3): 303–324.
• Bundy, A., A. Stevens, F. van Harmelen, A. Ireland and A. Smaill,1993, “Rippling: A Heuristic for Guiding InductiveProofs”,Artificial Intelligence, 62:185–253.
• Buresh-Oppenheim, J. and T. Pitassi, 2007, “The Complexityof Resolution Refinements”,Journal of Symbolic Logic,72 (4): 1336–1352.
• Chan, HL. and M. Norrish, 2019, “Classification of FiniteFields with Applications”,Journal of AutomatedReasoning, 63 (3): 667–693.
• Chang, C. L. and R. C. T. Lee, 1973,Symbolic Logic andMechanical Theorem Proving, New York: Academic Press.
• Chou, S., 1987,Mechanical Geometry Theorem Proving,Dordrecht: Kluwer Academic Publishers.
• Church, A., 1936a, “An unsolvable problem of elementarynumber theory”,American Journal of Mathematics, 58(2): 345–363.
• –––, 1936b, “A note on theEntscheidungsproblem”,Journal of Symbolic Logic, 1(1): 40–41.
• –––, 1940, “A Formulation of the SimpleTheory of Types”,Journal of Symbolic Logic, 5:56–68.
• Claessen, K. and N. Sörensson, 2003, “New Techniquesthat Improve MACE-style Finite Model Finding”,Proceedingsof the CADE-19 Workshop: Model Computation – Principles,Algorithms, Applications, P. Baumgartner and C. Fermueller(eds.)
• Clarke, E. and X. Zhao, 1994, “Combining SymbolicComputation and Theorem Proving: Some Problems of Ramanujan”,CADE-12: Proceedings of the 12th International Conference onAutomated Deduction, (Lecture Notes in Artificial Intelligence:Volume 814), A. Bundy (ed.), Berlin: Springer-Verlag, pp.758-763.
• Clocksin, W. F. and C. S. Mellish, 1981,Programming inProlog, Berlin: Springer-Verlag.
• Colmerauer, A., H. Kanoui, R. Pasero and P. Roussel, 1973,UnSystème de Communication Homme-machine en Français,Rapport, Groupe Intelligence Artificielle, Universitéd’Aix Marseille.
• Constable, R. L., S. F. Allen, H. M. Bromley, W.R. Cleaveland, J.F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P.Panangaden, J. T. Sasaki and S. F. Smith, 1986,ImplementingMathematics with the Nuprl Proof Development System, EnglewoodCliffs, NJ: Prentice Hall.
• Cook, S. A., 1971, “The complexity of Theorem-ProvingProcedures”,Proceedings of the 3rd Annual ACM Symposium onTheory of Computing, New York: Association for ComputingMachinery, pp. 151–158.
• Coquand, T. and G. Huet, 1988, “The Calculus ofConstructions”,Information and Computation - Semantics ofData Types, A. R. Meyer (ed.), 76 (2–3): 95–120.
• Coquand, T. and C. Paulin-Mohring, 1988, “InductivelyDefined Types”,COLOG88: Proceedings of the InternationalConference on Computer Logic, P. Martin-Löf and G. Mints(eds.), LNCS 417, pp. 50–66.
• Davis, M., G. Logemann and D. Loveland, 1962, “A MachineProgram for Theorem-Proving”,Communications of theAssociation for Computing Machinery, 5 (7): 394–397.
• Davis, M. and H. Putnam, 1960, “A Computing Procedure forQuantification Theory”,Journal of the Association forComputing Machinery, 7 (3): 201–215.
• de Bruijn, N. G., 1968, “Automath, a Language forMathematics”, inAutomation of Reasoning (Volume 2), J.Siekmann and G. Wrighston (eds.), Berlin: Springer-Verlag, 1983, pp.159–200.
• de Moura, L., 2007, “Developing Efficient SMTSolvers”,Proceedings of the CADE-21 Workshop on EmpiricallySuccessful Automated Reasoning in Large Theories, G. Sutcliffe,J. Urban and S. Schulz (eds.), Bremen.
• Denney, E., B. Fischer and J. Schumann, 2004, “UsingAutomated Theorem Provers to Certify Auto-generated AerospaceSoftware”,Automated Reasoning, Second International JointConference (IJCAR) (Lecture Notes in Artificial Intelligence:Volume 3097), D. Basin and M. Rusinowitch (eds.), Berlin:Springer-Verlag, pp. 198-212.
• Denney, E., J. Power and K. Tourlas, 2006, “Hiproofs: AHierarchical Notion of Proof Tree”,Proceedings of the 21stAnnual Conference on Mathematical Foundations of Programming Semantics(MFPS XXI) (Electronic Notes in Theoretical Computer Science,Vol. 155), pp. 341–359.
• Deutsch, D., 1982, “Quantum theory, the Church-Turingprinciple and the universal quantum computer”,Proceedingsof the Royal Society of London A, 400: 97–117.
• Dieks, D., 1982, “Communication by EPR devices”,Physics Letters A, 92: 271–272.
• Eisert, J., M. Wilkens and M. Lewenstein, 1999, “Quantumgames and quantum strategies”,Physical Review Letters,83: 3077–3080.
• –––, 2020, “Erratum: quantum games andquantum strategies”, [Physical Review Letters, 83:3077–3080],Physical Review Letters, 124: 139901.
• Ernst, Z., B. Fitelson, K. Harris and L. Wos, 2002,“Shortest Axiomatizations of Implicational S4 and S5”,Notre Dame Journal of Formal Logic, 43 (3):169–179.
• Farmer, W. M., J. D. Guttman and F. J. Thayer, 1993, “IMPS:An Interactive Mathematical Proof System”,Journal ofAutomated Reasoning, 11 (2): 213–248.
• Fitelson B. and E. Zalta, 2007, “Steps Toward aComputational Metaphysics”,Journal of PhilosophicalLogic, 36 (2): 227–247.
• Fitting, M., 1990,First-Order Logic and Automated TheoremProving, Berlin: Springer-Verlag.
• –––, 2002,Types, Tableaus andGödel’s God. Kluwer.
• Fuenmayor, D. and C. Benzmüller, 2017, “AutomatingEmendations of the Ontological Argument in Intensional Higher-OrderModal Logic”,KI 2017: Advances in Artificial Intelligence -Proceedings of the 40th Annual German Conference on AI, LNCS10505, G. Kern-Isberneret al. (eds.), pp. 114-127.
• Furbach , U., 1994, “Theory Reasoning in First OrderCalculi”,Management and Processing of Complex DataStructures, (Lecture Notes in Computer Science Volume 777), pp.139–156.
• Furbach, U., C. Schon and F. Stolzenburg, 2014, “AutomatedReasoning in Deontic Logic”,MIWAI2014: Proceedings of the8th Multi-disciplinary International Workshop on ArtificialIntelligence, LNAI 8875, M. N. Murtyet al. (eds.), pp.57–68.
• Ganesalingam, M. and W. T. Gowers, 2017, “A Fully AutomaticTheorem Prover with Human-Style Output”,Journal ofAutomated Reasoning, 58 (2): 253–291.
• Ganzinger, H., G. Hagen, R. Nieuwenhuis, A. Oliveras, C. Tinelli,2004, “DPLL(T): Fast Decision Procedures”,ComputerAided Verification, (Lecture Notes in Computer Science: Volume3114), pp. 175–188.
• Gentzen, G., 1935, “Investigations into LogicalDeduction”, in Szabo 1969, pp. 68–131.
• Giarratano, J. and G. Riley, 2004,Expert Systems: Principlesand Programming, 4th edition, Boston, MA: PWS Publishing Co.
• Gödel, K., 1970, “Appendix A: Notes in KurtGödel’s Hand“, in Sobel 2004, pp. 144–145.
• Gordon, M. J. C. and T. F. Melham, eds., 1993,Introduction toHOL: A Theorem Proving Environment for Higher Order Logic,Cambridge: Cambridge University Press.
• Gordon, M. J. C., A. J. Milner and C. P. Wadsworth, 1979,Edinburgh LCF: A Mechanised Logic of Computation (LNCS 78),Berlin: Springer-Verlag.
• Gorenstein, D., 1982,Finite Simple Groups: An Introduction totheir Classification (University Series in Mathematics), NewYork: Plenum Press.
• Green, C., 1969, “Application of Theorem Proving to ProblemSolving”,IJCAI’69 Proceedings of the 1stinternational joint conference on Artificial intelligence, SanFrancisco: Morgan Kaufmann, pp. 219–239
• Haack, S., 1978,Philosophy of Logics, Cambridge:Cambridge University Press.
• Hales, T. C., 2005a, “A proof of the KeplerConjecture”,Annals of Mathematics, 162 (3):1065–1185.
• –––, 2006, “Introduction to the FlyspeckProject”,Dagstuhl Seminar Proceedings 05021: Mathematics,Algorithms, Proofs, T. Coquandet al. (eds.)
• Hales, T. C.et al., 2015, “A Formal Proof of theKepler Conjecture”,arXiv:1501.02.02155 9 [mat.MG],Cornell University Library.
• Harrison, J., 2000, “High-Level Verification Using TheoremProving and Formalized Mathematics”,CADE-17: Proceedings ofthe 17th International Conference on Automated Deduction,(Lecture Notes in Artificial Intelligence: Volume 1831), D. McAllester(ed.), Berlin: Springer-Verlag, pp. 1-6.
• –––, 2006, “Verification: IndustrialApplications”,Proof Technology and Computation, H.Schwichtenberg and K. Spies (eds.), Amsterdam: IOS Press, pp.161–205.
• –––, 2009, “Formalizing an Analytic Proofof the Prime Number Theorem”,Journal of Automated Reasoning(Special Issue: A Festschrift for Michael J. C. Gordon), 43 (3):243–261.
• Harrison, J. and L. Théry, 1998, “A Skeptic’sApproach to Combining HOL and Maple”,Journal of AutomatedReasoning, 21: 279–294.
• Herbrand, J., 1930,Recherches sur la Theorie de laDemonstration, Travaux de la Societé des Sciences at desLettres de Varsovie, Classe III, Science Mathématique etPhysique, No. 33, 128.
• Heule, M. J. H. and O. Kullmann, 2017, “The Science of BruteForce”,Communications of the ACM, 60 (8):70–79.
• Heule, M. J. H., O. Kullmann and V. W. Marek, 2016, “Solvingand Verifying the Boolean Pythagorean Triples problem viaCube-and-Conquer”,Theory and Applications of SatisfiabilityTesting — SAT 2016, 19th International Conference, LNCS9710, N. Creignou and D. Le Berre (eds.), pp. 228–245.
• Hilbert, D. and W. Ackermann, 1928,Principles of MathematicalLogic, L. Hammond, G. Leckie, and F. Steinhardt (trans.), NewYork: Chelsea Publishing Co., 1950.
• Huet, G. P., 1975, “A Unification Algorithm for Typed\(\lambda\)-calculus”,Theoretical Computer Science, 1:27–57.
• Hunt Jr., W. A., M. Kaufmann, J. S. Moore and A. Slobodova, 2017,“Industrial Hardware and Software Verification with ACL2”,Philosophical Transactions of the Royal Society A, 375:20150399.
• Kaliszyk, C. and J. Urban, 2014, “Learning-AssistedAutomated Reasoning with Flyspeck”,Journal of AutomatedReasoning, 53 (2), 173–213.
• Kanckos, A., and B. W. Paleo, 2017, “Variants ofGödel’s Ontological Proof in a Natural DeductionCalculus”,Studia Logica, (3): 553–586.
• Kaufmann, M. and J. S. Moore, 1996, “ACL2: An industrialstrength version of Nqthm”,Proceedings of the 11th AnnualConference on Computer Assurance (COMPASS-96), IEEE ComputerSociety, pp. 23–34.
• Kerber, M., Kohlhase and V. Sorge, 1998, “IntegratingComputer Algebra into Proof Planning”,Journal of AutomatedReasoning, 21: 327–355.
• Kirchner, D., 2017, “Representation and Partial Automationof the Principia Logico-Metaphysica in Isabelle/HOL”,Archive of Formal Proofs. Formal proof development. ISSN:2150–914x. URL: http://isa-afp.org/entries/PLM.html.
• –––, 2021,Computer-Verified Foundations ofMetaphysics and an Ontology of Natural Numbers in Isabelle/HOL,Ph.D. Dissertation, Fachbereich Mathematik und Informatik, FreieUniversität Berlin.
• Kirchner, D., C. Benzmüller and E. Zalta, 2019,“Computer Science and Metaphysics: A Cross-Fertilization”,Open Philosophy, 2: 230–251.
• –––, 2020, “Mechanizing PrincipiaLogico-Metaphysica in Functional Type Theory",Review of SymbolicLogic, 13 (1): 206–18.
• Knuth, D. and P. B. Bendix, 1970, “Simple Word Problems inUniversal Algebras”, inComputational Problems in AbstractAlgebra, J. Leech (ed.), Oxford, New York: Pergamon Press, pp.263–297.
• Kleene, S. C., 1962,Introduction to Metamathematics,Amsterdam: North-Holland.
• Kovács, L. and A. Voronkov, 2013, “First-OrderTheorem Proving and VAMPIRE”,CAV 2013: Proceedings of theInternational Conference on Computer Aided Verification, N.Sharygina and H. Veith (eds.), LNCS 8044, pp. 1–35.
• Kowalski, R., 1974, “Predicate Logic as a ProgrammingLanguage”,Proceedings of the International Federation forInformation Processing (Proc. IFIP ’74), Amsterdam: NorthHolland, pp. 569–574.
• Küchlin, W. and C. Sinz, 2000, “Proving ConsistencyAssertions for Automotive Product Data Management”,Journalof Automated Reasoning (Special Issue: Satisfiability in the Year2000), I. P. Gent and T. Walsh (eds.), 24 (1–2):145–163.
• Kühlwein, D., T. van Laarhoven, E. Tsivtsivadze, J. Urban andT. Heskes, 2012, “Overview and Evaluation of Premise SelectionTechniques for Large Theory Mathematics”,AutomatedReasoning: 6th International Joint Conference, IJCAR 2012,(Lecture Notes in Computer Science: Volume 7364), B. Gramlich, D.Miller and U. Sattler (eds.), Manchester, UK: Springer-Verlag, pp.378–392.
• Lambán, L., F. J. Martín-Mateos, J. Rubio, and J. L.Ruiz-Reina, 2012, “Formalization of a Normalization Theorem inSimplicial Topology”,Annals of Mathematics and ArtificialIntelligence, 64 (1): 1–37.
• Lemmon, E. J., C. A. Meredith, D. Meredith, A. N. Prioir and I.Thomas, 1957,Calculi of Pure Strict Implication, PhilosophyDept., Canterbury University, Christchurch, New Zealand.
• Lloyd, J. W., 1984,Foundations of Logic Programming,Berlin: Springer-Verlag.
• Loveland, D. W., 1969, “A Simplified Format for the ModelElimination Procedure”,Journal of the Association forComputing Machinery, 16: 349–363.
• –––, 1970, “A Linear Format forResolution”,Proceedings of the IRIA Symposium on AutomaticDemonstration, New York: Springer-Verlag, pp. 147-162.
• –––, 1978,Automated Theorem Proving: ALogical Basis, Amsterdam: North Holland.
• Luckham, D., 1970, “Refinements in Resolution Theory”,Proceedings of the IRIA Symposium on Automatic Demonstration,New York: Springer-Verlag, pp. 163-190.
• Maggesi, M., 2018, “A Formalization of Metric Spaces in HOLLight”,Journal of Automated Reasoning, 60 (2):237–254.
• Martin-Löf, P., 1982, “Constructive Mathematics andComputer Programming”,Logic, Methodology and Philosophy ofScience (Volume IV), Amsterdam: North-Holland, pp. 153-175.
• Massacci, F. and L. Marraro, 2000, “Logical Cryptanalysis:Encoding and Analysis of the U.S. Data Encryption Standard”,Journal of Automated Reasoning (Special Issue: Satisfiabilityin the Year 2000), I. P. Gent and T. Walsh (eds.), 24 (1–2):165–203.
• McCarthy, J., 1962, “Towards a Mathematical Science ofComputation”,International Federation for InformationProcessing Congress (Munich, 1962), Amsterdam: North Holland, pp.21–28.
• McCharen, J. D., R. A. Overbeek and L. A. Wos, 1976,“Problems and Experiments for and with Automated Theorem-ProvingPrograms”,IEEE Transactions on Computers 8:773–782.
• McCune, W., 1997, “Solution of the Robbins Problem”,Journal of Automated Reasoning, 19 (3): 263–276.
• –––, 2001,MACE 2.0 Reference Manual andGuide, Mathematics and Computer Science Division, ANL/MSC-TM-249,Argonne National Laboratory.
• McRobie, M. A., 1991, “Automated Reasoning and NonclassicalLogics: Introduction”,Journal of Automated Reasoning,7 (4): 447–451.
• Medina-Bulo, I., F. Palomo-Lozano and J. Ruiz-Reina, 2010,“A Verified Common Lisp Implementation of Buchberger’sAlgorithm in ACL2”,Journal of Symbolic Computation, 45(1): 96–123.
• Meng, J. and L. C. Paulson, 2008, “Translating higher-orderclauses to first-order clauses”,Journal of AutomatedReasoning, 40 (1): 35–60.
• Meredith, C. A. and A. N. Prior, 1964, “Investigations intoImplicational S5”,Z. Math. Logik Grundlagen Math.,10:203–220.
• Meyer, J.-J. Ch., 2014, “Logics for Intelligent Agents andMulti-Agent Systems”,Handbook of the History of Logic,Volume 9: Computational Logic, J. Siekmann (ed.), pp.629–658, Elsevier.
• Miller, D. and G. Nadathur, 1988, “An Overview of\(\lambda\)Prolog”,Proceedings of the Fifth InternationalLogic Programming Conference — Fifth Symposium in LogicProgramming, R. Bowen and R. Kowalski (eds.), Cambridge, MA: MITPress.
• Minker, J., D. Seipel and C. Zaniolo, 2014, “Logic andDatabases: A History of Deductive Databases”,Handbook ofthe History of Logic, Volume 9: Computational Logic, J. Siekmann(ed.), pp. 571–627, Elsevier.
• Muzalewski, M., 1993,An Outline of PC Mizar, FondationPhilippe le Hodey, Brussels.
• Nipkow, T., L. C. Paulson and M. Wenzel, 2002,“Isabelle/HOL: A Proof Assistant for Higher-Order Logic“,LNCS Vol. 2283, pp. 207–208.
• Nivens, A. J., 1974, “A Human-Oriented Logic for AutomaticTheorem Proving”,Journal of the Association of ComputingMachinery, 21 (4): 606–621.
• Oppenheimer, P. and E. Zalta, 2011, “AComputationally-Discovered Simplification of the OntologicalArgument”,Australasian Journal of Philosophy, 89 (2):333–349.
• Paulson, L. C., 1990, “Isabelle: The Next 700 TheoremProvers”,Logic and Computer Science, P. Odifreddi(ed.), Academic Press, pp. 361–386.
• –––, 1994,Isabelle: A Generic TheoremProver (Lecture Notes in Computer Science: Volume 828), Berlin:Springer-Verlag.
• –––, 2010. “Three Years of Experience withSledgehammer, a Practical Link Between Automatic and InteractiveTheorem Provers”,PAAR-2010, B. Konevet al.(eds.), pp. 1–10.
• Paulson, L. C. and K. Grabczewski, 1996, “Mechanizing SetTheory”,Journal of Automated Reasoning, 17 (3):291–323.
• Pease, A. and G. Sutcliffe, 2007, “First Order Reasoning ona Large Ontology”,Proceedings of the CADE-21 Workshop onEmpirically Successful Automated Reasoning in Large Theories(Volume 257), G. Sutcliffe and J. Urban (eds.), Bremen.
• Pelletier, F. J., 1986, “Seventy-Five Problems for TestingAutomatic Theorem Provers”,Journal of AutomatedReasoning, 2 (2): 191–216.
• –––, 1998, “Natural Deduction TheoremProving in THINKER”,Studia Logica, 60 (1):3–43.
• Pelletier, F. J., G. Sutcliffe and A. P. Hazen, 2017,“Automated Reasoning for the Dialetheic Logic RM3”,Proceedings of the Thirtieth International Florida ArtificialIntelligence Research Society Conference, V. Rus and Z. Markov(eds.), pp. 110–115.
• Pelletier, F. J., G. Sutcliffe, and C. Suttner, 2002, “TheDevelopment of CASC”,AI Communications, 15(2–3): 79–90.
• Peterson, J. G., 1977,The Possible Shortest Single Axiom forEC-Tautologies, Report 105, Department of Mathematics, Universityof Auckland.
• Pollock, J., 1989, “OSCAR: A General Theory ofRationality”,Journal of Experimental & TheoreticalArtificial Intelligence, 1 (3): 209–226
• –––, 1995,Cognitive Carpentry,Cambridge, MA: Bradford/MIT Press.
• –––, 2006, “Against Optimality: LogicalFoundations for Decision-Theoretic Planning in AutonomousAgents”,Computational Intelligence, 22(1):1–25.
• Portoraro, F. D., 1994, “Symlog: Automated Advice inFitch-style Proof Construction”,CADE-12: Proceedings of the12th International Conference on Automated Deduction, (LectureNotes in Artificial Intelligence: Volume 814), A. Bundy (ed.), Berlin:Springer-Verlag, pp. 802-806.
• –––, 1998, “Strategic Construction ofFitch-style Proofs”,Studia Logica, 60 (1):45–66.
• Prasad, M., A. Biere and A. Gupta, 2005, “A Survey of RecentAdvances in SAT-Based Formal Verification”,InternationalJournal on Software Tools for Technology Transfer, 7 (2):156–173.
• Prawitz, D., 1965,Natural Deduction: A Proof TheoreticalStudy, Stockholm: Almqvist & Wiksell.
• Quaife, A., 1992,Automated Development of FundamentalMathematical Theories, Kluwer Academic Publishers.
• Robinson, J. A., 1965, “A Machine Oriented Logic Based onthe Resolution Principle”,Journal of the Association ofComputing Machinery, 12: 23–41.
• –––, 1965, “Automatic Deduction withHyper-resolution”,Internat. J. Comput. Math., 1:227–234.
• Robinson, J. A. and A. Voronkov (eds.), 2001,Handbook ofAutomated Reasoning: Volumes I and II, Cambridge, MA: MITPress.
• Russinoff, D. M., 2017, “A Computationally Surveyable Proofof the Group Properties of an Elliptic Curve”,Proceedingsof the 14th International Workshop on the ACL2 Theorem Prover and ItsApplications, W. Hunt Jr. and A. Slobodova (eds.), OpenPublishing Association (EPTCS 249), pp. 30–46.
• –––, 2023, “A Formalization of FiniteGroup Theory: Part III”,Proceedings of the 18thInternational Workshop on the ACL2 Theorem Prover and ItsApplications, A. Coglio and S. Swords (eds.), Open PublishingAssociation (EPTCS 393), pp. 33–49.
• Schmitt, P. and I. Tonin, 2007, “Verifying the Mondex CaseStudy”,Proceedings of the Fifth IEEE InternationalConference on Software Engineering and Formal Methods, IEEEComputer Society, pp. 47–58.
• Schulz, S., 2004, “System Abstract: E 0.81”,Proceedings of the 2nd International Joint Conference on AutomatedReasoning (Lecture Notes in Artificial Intelligence: Volume3097), D. Basin and M. Rusinowitch (eds.), Berlin: Springer-Verlag,pp.223-228.
• Scott, D., 1972, “Appendix B: Notes in Dana Scott’sHand”, in Sobel 2004, pp. 145–146.
• Sieg, W. and J. Byrnes, 1996,Normal Natural Deduction Proofs(in Classical Logic), Report CMU-PHIL 74, Department ofPhilosophy, Carnegie-Mellon University.
• Slaney, J. K., 1984, “3,088 Varieties: A Solution to theAckerman Constant Problem”,Journal of Symbolic Logic,50: 487–501.
• Sobel, J. H., 2004,Logic and Theism: Arguments for andAgainst Beliefs in God, Cambridge University Press.
• Steen, A. and C. Benzmüller, 2021, “ExtensionalHigher-Order Paramodulation in Leo-III”,Journal ofAutomated Reasoning, 65 (6): 775–807.
• Stickel, M. E., 1992, “A Prolog Technology Theorem Prover: ANew Exposition and Implementation in Prolog”,TheoreticalComputer Science, 104: 109–128.
• Suppes, P.,et al., 1981, “Part I: InteractiveTheorem Proving in CAI Courses”,University-LevelComputer-Assisted Instruction at Stanford: 1968–1980, P.Suppes (ed.), Institute for the Mathematical Study of the SocialSciences, Stanford University.
• Sutcliffe, G., 2017, “The TPTP Problem Library andAssociated Infrastructure”,Journal of AutomatedReasoning, 59 (4): 483–502.
• Sutcliffe, G. and C. Benzmüller, 2010, “AutomatedReasoning in Higher-Order Logic Using TPTP THF Infrastructure”,Journal of Formalized Reasoning, 43 (4): 337–362.
• Sutcliffe, G. and C. Suttner, 1998, “The TPTP ProblemLibrary – CNF Release v1.2.1”,Journal of AutomatedReasoning, 21 (2): 177–203.
• Szabo, M. E. (ed.), 1969,The Collected Papers of GerhardGentzen, Amsterdam: North-Holland.
• Trybulec, A., 1978, “The Mizar Logic InformationLanguage”,Bulletin of the Association for LiteraryLinguistic Computing, 6(2): 136–140.
• Trybulec, A. and H. Blair, 1985, “Computer AssistedReasoning with Mizar”,Proceedings of the 9th InternationalJoint Conference on Artificial Intelligence, (IJCAI-85: Volume1), Los Angeles, pp. 26–28.
• Turing, A., 1936, “On computable numbers, with anapplication to the Entscheidungsproblem”,Proceedings of theLondon Mathematical Society, 42 (2): 230–265.
• Urban, J., 2007, “MaLARea: A Metasystem for AutomatedReasoning in Large Theories”,Proceedings of the CADE-21Workshop on Empirically Successful Automated Reasoning in LargeTheories, J. Urban, G. Sutcliffe and S. Schulz (eds.), pp.45–58.
• Urban, J., K. Hoder, A. Voronkov, 2010, “Evaluation ofAutomated Theorem Proving on the Mizar Mathematical Library”,Mathematical Software – ICMS 2010: Proceedings of the ThirdInternational Congress on Mathematical Software, Kobe, Japan,(Lecture Notes in Computer Science, Volume 6327), pp.155–166.
• Urban, J. and J. Vyskocil, 2012, “Theorem Proving in LargeFormal Mathematics as an Emerging AI Field”,arXiv:1209.3914[cs.AI], Report No. DPA-12271, Cornell University.
• Urquhart, A., 1987, “Hard Examples for Resolution”,Journal of the ACM, 34 (1): 209–219.
• –––, 1994 (ed.),The Collected Papers ofBertrand Russell, Volume 4: Foundations of Logic, 1903-05,Routledge, London and New York.
• van Benthem Jutting, L. S., 1977,Checking Landau’s“Grundlagen” in the Automath system, Ph.D. Thesis,Eindhoven University of Technology; published inMathematicalCentre Tracts, Number 83, Amsterdam: Mathematisch Centrum, 1979.
• Voronkov, A., 1995, “The Anatomy of Vampire: ImplementingBottom-Up Procedures with Code Trees”,Journal of AutomatedReasoning, 15 (2): 237–265.
• Wallen, L. A., 1990,Automated Deduction in NonclassicalLogics, Cambridge, MA: MIT Press.
• Wang, H., 1960, “Proving Theorems by Pattern Recognition– I”, inAutomation of Reasoning (Volume 1), J.Siekmann and G. Wrightson (eds.), Berlin: Springer-Verlag, 1983, pp.229–243.
• –––, 1960, “Toward MechanicalMathematics”, inAutomation of Reasoning (Volume 1), J.Siekmann and G. Wrightson (eds.), Berlin: Springer-Verlag, 1983, pp.244-264.
• Wegner, B., 2011, “Completeness of reference databases,old-fashioned or not?”,Newsletter of the EuropeanMathematical Society, 80: 50–52.
• Wiedijk, F., 2006,The Seventeen Provers of the World,(Lecture Notes in Artificial Intelligence: Volume 3600), F. Wiedijk(ed.), New York: Springer-Verlag.
• –––, 2007, “The QED ManifestoRevisited”,Studies in Logic, Grammar and Rhetoric, 10(23): 121–133.
• Wooters, W.K. and W. H. Zurek, 1982, “A single quantumcannot be cloned”,Nature, 299: 802–803.
• Wos, L. (ed.), 2001,Journal of Automated Reasoning(Special Issue: Advances in Logic Through Automated Reasoning), 27(2).
• Wos, L., D. Carson and G. R. Robinson, 1965, “Efficiency andCompleteness of the Set of Support Strategy in Theorem Proving”,Journal of the Association of Computing Machinery, 12:698–709.
• Wos, L., R. Overbeek, E. Lusk and J. Boyle, 1984,AutomatedReasoning: Introduction and Applications, Englewood Cliffs, NJ:Prentice-Hall.
• Wos, L., D. Ulrich, and B. Fitelson, 2002, “Vanquishing theXCB Question; The Methodological Discovery of the Last Shortest SingleAxiom for the Equivalential Calculus”,Journal of AutomatedReasoning, 29 (2):107–124.
• Wos, L., S. Winker, R. Veroff, B. Smith and L. Henschen, 1983,“Questions Concerning Possible Shortest Single Axiom for theEquivalential Calculus: An Application of Automated Theorem Proving toInfinite Domains”,Notre Dame Journal of Formal Logic,24: 205–223.
• Yoo, J., E. Jee and S. Cha, 2009, “Formal Modeling andVerification of Safety-Critical Software”,IEEESoftware, 26 (3): 42–49.
• Zalta, E., 1983,Abstract Objects: An Introduction toAxiomatic Metaphysics, Synthese Library, SYLI Volume 160,Springer.
• –––, 1999, “Natural Numbers and NaturalCardinals as Abstract Objects: A Partial Reconstruction ofFrege’s Grundgesetze in Object Theory”,Journal ofPhilosophical Logic, 28 (6): 619–660.
• –––, 2018, “How ComputationalInvestigations Improved an Ontology”,2018 Annual Meeting ofthe International Association for Computing and Philosophy,Warsaw, Polska Akademia Nauk (PAN), Copernicus Center,
• –––, 2022,PrincipiaLogico-Metaphysica, Draft/Excerpt dated September 2, 2022, URL:https://mally.stanford.edu/principia.pdf
• Zhang, L. and S. Malik, 2002, “The Quest for EfficientBoolean Satisfiability Solvers”,CADE-18: Proceedings of the18th International Conference on Automated Deduction, (LectureNotes in Artificial Intelligence: Volume 2392), A. Voronkov (ed.),Berlin: Springer-Verlag, pp. 295-313.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

Publications

• Hales, T. C., 2005b,The Flyspeck Project Fact Sheet
• Hales, T. C., 2014,Flyspeck
• Kaufman, M. and J. S. Moore, 2024, “A Walking Tour of ACL2”,ACL2 User’s Manual.
• Martin, U. and A. Pease, 2013, “What does mathoverflow tell us about the production of mathematics?,”Computing Research Repository, at arxiv.org.
• Sutcliffe, G., 2014,Proceedings of the 7th IJCAR AutomatedTheorem Proving System Competition (CASC-J7),available online, pp. 1–36.
• Sutcliffe, G., 2016,Proceedings of the 8th IJCAR AutomatedTheorem Proving System Competition (CASC-J8),available online, pp. 1–40.

Web Sites

• ACL2: A Computational Logic
• Alfa/Agda
• The Coq Proof Assistant (now known as the Rocq Prover)
• CVC4
• E Theorem Prover
• EQP Equational Prover
• HOL Automated Reasoning Group
• HOL Light
• IMPS: An Interactive Mathematical Proof System
• iProver
• Isabelle
• leanCoP
• LEO-II
• LEO-III
• Metamath
• MetiTarski
• The Minlog System
• The Mizar Project
• The Nuprl Project
• Paradox
• Prover 9 and Mace 4
• PVS Specification and Verification System
• Satallax
• Sledgehammer
• SPASS
• TPS Theorem Proving System
• Vampire
• Yices 2
• Z3
• The CADE ATP System Competition
• The TPTP Problem Library for Automated Theorem Proving
• The SMT-LIB Satisfiability Modulo Theories Library
• The QED Manifesto
• CADE: The Conference on Automated Deduction
• IJAR: The International Joint Conference on Automated Reasoning

Related Entries

artificial intelligence: logic-based |logic: classical |logic: modal |reasoning: defeasible