# tptp

[![Build Status](https://travis-ci.org/aztek/tptp.svg?branch=master)](https://travis-ci.org/aztek/tptp)

[TPTP](http://www.tptp.org) (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](http://hackage.haskell.org/package/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.

```haskell
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
  ]
```