Copyright | (c) Evgenii Kotelnikov 2019-2021 |
---|---|

License | GPL-3 |

Maintainer | evgeny.kotelnikov@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

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

## Synopsis

- module ATP.FOL
- module ATP.Pretty.FOL
- module ATP.Prove
- module ATP.Prover
- module ATP.Error

# First-order logic

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

module ATP.FOL

# Pretty printing for formulas, theorems and proofs

`pprint`

pretty-prints theorems and proofs.

`>>>`

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

module ATP.Pretty.FOL

# Interface to automated theorem provers

`prove`

runs a `defaultProver`

and parses the proof that it produces.

`>>>`

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]`prove syllogism >>= pprint`

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.

module ATP.Prove

# Models of automated theorem provers

By default `prove`

runs the E theorem prover (`eprover`

). Currently,
`eprover`

and `vampire`

are supported.

`proveUsing`

runs a specified theorem prover.

module ATP.Prover

# Error handling

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`

.

module ATP.Error