The online-atps package

[maintain]

This package provides an interface to use the automatic theorem provers (ATPs) of TPTP World.


[Skip to ReadMe]

Properties

Version0.1.1.3
Dependenciesaeson (>=1.0.1.0 && <1.2), base (>=4.6.0.1 && <4.10), bytestring (>=0.10.0.2 && <0.11), directory (>=1.2.0.1 && <1.4), filepath (>=1.3.0.1 && <1.5), HTTP (>=4000 && <5000), http-client (>=0.5.1 && <1.0), mtl (>=2.2.1 && <2.3), network (>=2.6.0 && <3.0), pretty (>=1.1.1.0 && <1.1.1.2 || >=1.1.2 && <1.2), split (>=0.2 && <1.0), tagsoup (>=0.14 && <1.0), text (>=0.11.3.1 && <1.3), unordered-containers (==0.2.*), yaml (>=0.8.17 && <0.9) [details]
LicenseMIT
AuthorJonathan Prieto-Cubides
MaintainerJonathan Prieto-Cubides <jprieto9@eafit.edu.co>
CategoryLogic, Theorem Provers
Home pagehttps://github.com/jonaprieto/online-atps
Bug trackerhttps://github.com/jonaprieto/online-atps/issues/
Source repositoryhead: git clone git://github.com/jonaprieto/online-atps.git
Executablesonline-atps
UploadedTue Jan 24 23:04:17 UTC 2017 by jonaprieto

Flags

NameDescriptionDefaultType
devwhen develop takes places.DisabledManual

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for online-atps-0.1.1.3

OnlineATPs Build Status

OnlineATPs is a client for SystemOnTPTP that allows us to take advantage of using ATPs without install any of them.

Requirements

$ cabal update
$ cabal install cabal-install

Installation

$ git clone https://github.com/jonaprieto/online-atps.git
$ cd online-atps
$ cabal install

Also, yo may interested in checking the Makefile and execute make install-bin.

Usage

The work flow using OnlineATPs consists mainly in provide a problem in TSTP format, and ATP name and then wait over a second while the request takes place in TPTP world and returns with a response. Let's see.

$ online-atps --list-atps
$ online-atps --help
Usage: online-atps [OPTIONS] FILE

    --atp=NAME          Set the ATP (online-e, online-vampire, online-z3, ...)
    --fof               Only use ATP for FOF
    --help              Show this help
    --list-atps         Consult all ATPs available in TPTP World
    --only-check        Only checks the output looking for a theorem.
    --time=NUM          Set timeout for the ATPs in seconds (default: 300)
    --version           Show version number
    --version-atp=NAME  Show version of the atp NAME
    --
$ cat basic.tptp
fof(a1, axiom, a).
fof(a2, axiom, b).
fof(a3, axiom, (a & b) => z).
fof(a4, conjecture, z).

Prove the conjecture with the help of ATPs. You could use one from the list (--list-atps option) or with all ATPs available. For instance, let's try with Vampire:

$ online-atps basic.tptp --atp=vampire
% SZS start RequiredInformation
% Congratulations - you have become a registered power user of SystemOnTPTP,
at IP address 138.121.12.14.
% Please consider donating to the TPTP project - see www.tptp.org for
details.
% When you donate this message will disappear.
% If you do not donate a random delay might be added to your processing time.
% SZS end RequiredInformation
Vampire---4.1   system information being retrieved
Vampire---4.1's non-default parameters being retrieved
    -t none
    -f tptp:raw
    -x vampire --mode casc -m 90000 -t %d %s
Vampire---4.1   being checked for execution
Vampire---4.1   checking time limit 240
Vampire---4.1   checking problem name /tmp/SystemOnTPTPFormReply38743/
SOT_Xry401
...
% ------------------------------
% Version: Vampire 4.1 for CASC J8 Entry
% Termination reason: Refutation

% Memory used [KB]: 511
% Time elapsed: 0.043 s
% ------------------------------
% ------------------------------
% Success in time 0.045 s

% END OF SYSTEM OUTPUT
RESULT: SOT_Xry401 - Vampire---4.1 says Theorem - CPU = 0.00 WC = 0.04
OUTPUT: SOT_Xry401 - Vampire---4.1 says Refutation - CPU = 0.00 WC = 0.04

Contributions

Check the issues. Thanks.