The online-atps package

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain]

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


[Skip to ReadMe]

Properties

Version0.1.1.3
Change logNone available
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
dev

when 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

[back to package description]

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.