atp-0.1.0.0: Interface to automated theorem provers
Copyright(c) Evgenii Kotelnikov 2019-2021
LicenseGPL-3
Maintainerevgeny.kotelnikov@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

ATP.Codec.TPTP

Description

 
Synopsis

Documentation

encode :: LogicalExpression -> Formula Source #

Encode a formula in unsorted first-order logic in TPTP.

decode :: Formula -> Partial LogicalExpression Source #

Decode a formula in unsorted first-order logic from TPTP.

encodeFormula :: Formula -> UnsortedFirstOrder Source #

Encode a formula in unsorted first-order logic in TPTP.

decodeFormula :: UnsortedFirstOrder -> Partial Formula Source #

Decode a formula in unsorted first-order logic from TPTP.

encodeClause :: Clause -> Clause Source #

Encode a clause in unsorted first-order logic in TPTP.

decodeClause :: Clause -> Partial Clause Source #

Decode a clause in unsorted first-order logic from TPTP.

encodeTheorem :: Theorem -> TPTP Source #

Encode a theorem in unsorted first-order logic in TPTP.

encodeClauses :: Clauses -> TPTP Source #

Encode a set of first-order clauses in TPTP.

decodeSolution :: TSTP -> Partial Solution Source #

Decode a solution from a TSTP output.