Express theorems in first-order logic and automatically prove them using third-party reasoning tools.

Consider the following classical logical syllogism.

All humans are mortal. Socrates is a human. Therefore, Socrates is mortal.

We can formalize it in first-order logic as follows.

human, mortal :: UnaryPredicate
human = UnaryPredicate "human"
mortal = UnaryPredicate "mortal"

socrates :: Constant
socrates = "socrates"

humansAreMortal, socratesIsHuman, socratesIsMortal :: Formula
humansAreMortal = forall $ \x -> human x ==> mortal x
socratesIsHuman = human socrates
socratesIsMortal = mortal socrates

syllogism :: Theorem
syllogism = [humansAreMortal, socratesIsHuman] |- socratesIsMortal

pprint pretty-prints theorems and proofs.

>>> pprint syllogism
Axiom 1. ∀ x . (human(x) => mortal(x))
Axiom 2. human(socrates)
Conjecture. mortal(socrates)

prove runs a defaultProver and parses the proof that it produces.

>>> prove syllogism >>= pprint
Found a proof by refutation.
1. human(socrates) [axiom]
2. ∀ x . (human(x) => mortal(x)) [axiom]
3. mortal(socrates) [conjecture]
4. ￢mortal(socrates) [negated conjecture 3]
5. ∀ x . (￢human(x) ⋁ mortal(x)) [variable_rename 2]
6. mortal(x) ⋁ ￢human(x) [split_conjunct 5]
7. mortal(socrates) [paramodulation 6, 1]
8. ⟘ [cn 4, 7]

The proof returned by the theorem prover is a directed acyclic graph of logical inferences. Each logical Inference is a step of the proof that derives a conclusion from a set of premises using an inference Rule. The proof starts with negating the conjecture and ends with a Contradiction and therefore is a proof by Refutation.

Theorem provers implement elaborate proof search strategies that can be tweaked in many different ways. ProvingOptions contain values of the input parameters to theorem provers. prove uses defaultOptions and proveWith run a specified set of options.

By default prove runs the E theorem prover (eprover). Currently, eprover and vampire are supported.

proveUsing runs a specified theorem prover.

A theorem prover might not succeed to construct a proof. Therefore the result of prove is wrapped in the Partial monad that represents a possible Error, for example TimeLimitError or ParsingError.