tptp: A parser and a pretty printer for the TPTP language
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.
[Skip to Readme]
Modules
[Index] [Quick Jump]
Flags
Manual Flags
| Name | Description | Default |
|---|---|---|
| werror | Disabled |
Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info
Downloads
- tptp-0.1.0.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
| Versions [RSS] | 0.1.0.0, 0.1.0.1, 0.1.0.2, 0.1.0.3, 0.1.1.0, 0.1.2.0, 0.1.3.0 |
|---|---|
| Change log | CHANGELOG.md |
| Dependencies | attoparsec (>=0.13.2 && <0.14), base (>=4.5 && <5.0), directory (>=1.2.5 && <1.4), extra (>=1.4.4 && <1.7), prettyprinter (>=1.2.1 && <1.3), scientific (>=0.3.6 && <0.4), semigroups (>=0.16.1 && <0.19), text (>=1.2.3 && <1.3), tptp [details] |
| License | GPL-3.0-only |
| Author | Evgenii Kotelnikov |
| Maintainer | evgeny.kotelnikov@gmail.com |
| Category | Language, Parsing, Pretty Printer, Theorem Provers, Formal Methods |
| Home page | https://github.com/aztek/tptp |
| Bug tracker | https://github.com/aztek/tptp/issues |
| Source repo | head: git clone git://github.com/aztek/tptp.git |
| Uploaded | by EK at 2019-05-07T11:39:57Z |
| Distributions | |
| Reverse Dependencies | 1 direct, 0 indirect [details] |
| Executables | parse-tptp-library, parser |
| Downloads | 2276 total (19 in the last 30 days) |
| Rating | (no votes yet) [estimated by Bayesian average] |
| Your Rating | |
| Status | Docs available [build log] Last success reported on 2019-05-07 [all 1 reports] |
Readme for tptp-0.1.0.0
[back to package description]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
]