tptp

TPTP (Thousands of Problems for Theorem Provers) is the standard language of problems, proofs, and models, used by automated theorem provers.

This library provides definitions of data types, a pretty printer and an attoparsec parser for (currently, a subset of) the TPTP language.

Example

Consider the following classical syllogism.

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

We can formalize this syllogism in unsorted first-order logic and write it down in TPTP as following.

import Data.TPTP

humansAreMortal :: UnsortedFirstOrder
humansAreMortal = forall ["P"] $
  Connective (Predicate "human" [var "P"]) Implication (Predicate "mortal" [var "P"])

socratesIsHuman :: UnsortedFirstOrder
socratesIsHuman = Predicate "human" [Function "socrates" []]

socratesIsMortal :: UnsortedFirstOrder
socratesIsMortal = Predicate "mortal" [Function "socrates" []]

syllogism :: TPTP
syllogism = TPTP [
    axiom "humans_are_mortal" humansAreMortal,
    axiom "socrates_is_human" socratesIsHuman,
    conjecture "socrates_is_mortal" socratesIsMortal
  ]