Skip to content

jonaprieto/online-atps

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

93 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

OnlineATPs Build Status DOI

OnlineATPs is a command-line client for TPTP World. We can use an online ATP as it would be running locally. Indeed, SystemOnTPTP has available more than forty automatic theorem provers and we take avantage of all.

Requirements

  • OnlineATPs has been built and tested using GHC 8.6.5. Please, check your version with:
$ ghc --version
  • Use the last version of Cabal. OnlineATPs has been installed successfully using cabal-1.22 and cabal-1.24.
$ cabal update
$ cabal install cabal-install
$ cabal --version

Installation

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

Usage

  • To take advantage of OnlineATPs, we recommend check first SystemOnTPTP to see what is about.

  • The user provide a problem formatted using TPTP syntax. Also, specify at least one ATP name. Then, execute online-atps to get an output, as we can see this output is pretty similar to the answer given by a local ATP but more verbose. Let see.

    • For instance, a TPTP problem looks similar to:
    $ cat basic.tptp
    fof(a1, axiom, a).
    fof(a2, axiom, b).
    fof(a3, axiom, (a & b) => z).
    fof(a4, conjecture, z).
    
    • Using the option --atp we specify the ATP. For instance, using --atp=vampire we specify that we are going to use Vampire ATP against the problem.
    $ 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
    
    
  • See all ATPs available. Run this command:

$ online-atps --list-atps
  • Check the help command to see all options of online-atps:
$ online-atps --help
  • OnlineATPs accepts a name for a ATP using the prefix "online-" or not (e.g "vampire" or "online-vampire")
$ online-atps basic.tptp --atp=online-metis
  • Check if a problem states a theorem or not using --only-check
$ online-atps basic.tptp --atp=online-metis --only-check

Contribute

Any contribution to improve this package is welcomed. Just check the issues or create a new one.