Editing First-order logic (section)

==Automated theorem proving and formal methods==
{{further|Automated theorem proving#First-order theorem proving}}

[[Automated theorem proving]] refers to the development of computer programs that search and find derivations (formal proofs) of mathematical theorems.<ref name="Fitting2012">{{cite book|author=Melvin Fitting|title=First-Order Logic and Automated Theorem Proving|url=https://books.google.com/books?id=133kBwAAQBAJ|date=6 December 2012|publisher=Springer Science & Business Media|isbn=978-1-4612-2360-3}}</ref> Finding derivations is a difficult task because the [[search algorithm|search space]] can be very large; an exhaustive search of every possible derivation is theoretically possible but [[Computational complexity theory|computationally infeasible]] for many systems of interest in mathematics. Thus complicated [[heuristic function]]s are developed to attempt to find a derivation in less time than a blind search.<ref>{{Cite web |title=15-815 Automated Theorem Proving |url=https://www.cs.cmu.edu/~fp/courses/atp/ |access-date=2024-01-10 |website=www.cs.cmu.edu}}</ref>

The related area of automated [[proof verification]] uses computer programs to check that human-created proofs are correct. Unlike complicated automated theorem provers, verification systems may be small enough that their correctness can be checked both by hand and through automated software verification. This validation of the proof verifier is needed to give confidence that any derivation labeled as "correct" is actually correct.

Some proof verifiers, such as [[Metamath]], insist on having a complete derivation as input. Others, such as [[Mizar system|Mizar]] and [[Isabelle (theorem prover)|Isabelle]], take a well-formatted proof sketch (which may still be very long and detailed) and fill in the missing pieces by doing simple proof searches or applying known decision procedures: the resulting derivation is then verified by a small core "kernel". Many such systems are primarily intended for interactive use by human mathematicians: these are known as [[proof assistant]]s. They may also use formal logics that are stronger than first-order logic, such as type theory. Because a full derivation of any nontrivial result in a first-order deductive system will be extremely long for a human to write,<ref>[[Jeremy Avigad|Avigad]], ''et al.'' (2007) discuss the process of formally verifying a proof of the [[prime number theorem]]. The formalized proof required approximately 30,000 lines of input to the Isabelle proof verifier.</ref> results are often formalized as a series of lemmas, for which derivations can be constructed separately.

Automated theorem provers are also used to implement [[formal verification]] in computer science. In this setting, theorem provers are used to verify the correctness of programs and of hardware such as [[CPU|processors]] with respect to a [[formal specification]]. Because such analysis is time-consuming and thus expensive, it is usually reserved for projects in which a malfunction would have grave human or financial consequences.

For the problem of [[model checking]], efficient [[algorithm]]s are known to [[decision problem|decide]] whether an input finite structure satisfies a first-order formula, in addition to [[computational complexity]] bounds: see {{section link|Model checking|First-order logic}}.