online-atps: OnlineATPs is a client for TPTP World and its ATPs

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] [Publish]

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

[Skip to Readme]

Properties

Versions	0.1.1.3
Change log	None available
Dependencies	aeson (>=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 && <0.3), yaml (>=0.8.17 && <0.9) [details]
License	MIT
Author	Jonathan Prieto-Cubides
Maintainer	Jonathan Prieto-Cubides <jprieto9@eafit.edu.co>
Category	Logic, Theorem Provers
Home page	https://github.com/jonaprieto/online-atps
Bug tracker	https://github.com/jonaprieto/online-atps/issues/
Source repo	head: git clone git://github.com/jonaprieto/online-atps.git
Uploaded	by jonaprieto at 2017-01-24T23:04:17Z

Flags

Manual Flags

Name	Description	Default
dev	when develop takes places.	Disabled

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

Downloads

online-atps-0.1.1.3.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

jonaprieto

For package maintainers and hackage trustees

edit package information

Readme for online-atps-0.1.1.3

[back to package description]

OnlineATPs

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

Requirements

OnlineATPs has been built and tested using GHC 7.6.3, 7.8.4, 7.10.3, and 8.0.2.
Please install the last version of Cabal. OnlineATPs has been installed successfully using cabal-1.22 and cabal-1.24.

$ 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.

See all ATPs available running the command

$ online-atps --list-atps

Check the help command to see all options of online-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
    --

Prove a small conjecture (in TSTP format) like this:

$ 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

Online ATPs accepts a name for a ATP using the prefix "online-" or not (e.g "vampire" or "online-vampire").

Contributions

Check the issues. Thanks.