edechter / iprover Goto Github PK
View Code? Open in Web Editor NEWAutomatically exported from code.google.com/p/iprover
License: GNU General Public License v3.0
Automatically exported from code.google.com/p/iprover
License: GNU General Public License v3.0
--------------------iProver----------------------- iProver is a reasoner for first-order logic. ------------------------------------------------- Download the current version from: http://code.google.com/p/iprover/ ------------------------------------------------- Easy to install: ------------------------------------------------- We assume OCaml v4.00 >= is installed. 1) ./configure 2) make will produce executable: iproveropt -1) "make clean" to remove created objects and executable files -2) "make clean_all" to remove created objects and executable files including E objects (if iProver does not compile try this first) ------------------------------------------------- Easy to use: ------------------------------------------------- iproveropt problem.p where problem.p is a problem in the TPTP format ------------------------------------------------- Examples: ------------------------------------------------- General: 1) iproveropt problem.p Sat modes: 2) iproveropt --schedule sat problem_sat.p 3) iproveropt --sat_mode true --schedule none --sat_finite_models true problem_sat.p FOF format: 4a) iproveropt --clausifier /home/eprover/eprover \ --clausifier_options " --tstp-format --silent --cnf " problem_fof.p Clausifier is any executable that transforms formulas into TPTP cnf form, --clausifier_options are the options passed to the clausifier. If you are using bundled version then you do not need to specify these options. 4b) iproveropt --clausifier /home/vampire/vampire --clausifier_options "--mode clausify" problem_fof.p 5) iproveropt --help ------------------------------------------------- It might be convenient to collect options you like in a file (e.g. example.opt) and run iproveropt $(cat example.opt) problem.p The default options should be generally ok. ----------------------------------------------------- Output ---------------------------------------------------- Output: the output of iProver is according to a modified version of SZS ontology: "SZS status Theorem" corresponds to a proved theorem where the input is first-order and contains a theorem represented by a conjecture. "SZS status CounterSatisfiable" corresponds to disproving the theorem where the input is first-order and contains a theorem represented by a conjecture. "SZS status Unsatisfiable" corresponds to an unsatisfiable set of input formulas where the input does not contain a theorem (i.e. either cnf or fof and does not contain a conjecture) "SZS status Satisfiable" corresponds to a satisfiable set of input formulas where the input does not contain a theorem (i.e. contains neither a conjecture or a negated_conjecture) % SZS output start Model Model representation output when a model is found by instantiation % SZS output end Model -------------------------------------------------------------------------------------------- Please send any comments, report bugs to korovin[@]cs.man.ac.uk If you are interested in a different from GNU GPL license please email korovin[@]cs.man.ac.uk -------------------------------------------------------------------------------------------- ------------------------------------------------- Additional Info ------------------------------------------------- iProver is based on an instantiation calculus Inst-Gen, which is complete for first-order logic: http://www.cs.man.ac.uk/~korovink/my_pub/instantiation_lics03.ps iProver has been developed and implemented by Konstantin Korovin (korovin[@]cs.man.ac.uk), The University of Manchester, UK In 2008 Christoph Sticksel has joined the project. iProver combines instantiation with resolution and implements a number of redundancy elimination methods: http://www.cs.man.ac.uk/~korovink/my_pub/inv_to_inst.ps (see also the list of options for details) For ground reasoning iProver uses C version of MiniSat: http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ iProver accepts problems in TPTP format: http://www.cs.miami.edu/~tptp/ For problems in fof (and not just cnf) format, iProver can use any external clausifier, see examples. External clausifier is NOT required if the input is in cnf and a clausifier (as an option to E prover) is included only in the bundled distribution. iProver has a satisfiability mode which includes a finite model finder, incorporating some ideas from Paradox and DarwinFM. To activate satisfiability mode use "iproveropt --sat_mode true problem_sat.p". to search for finite models you can run "iproveropt --sat_mode true --schedule none --sat_finite_models true problem_sat.p". iProver outputs models when satisfiability is shown by instantiation. Different representations of models are implemented based on definitions of predicates in term algebra. ----------------------------------------------------- iProver combines instantiation with resolution If you would like to run pure instantiation/resolution then you can switch the corresponding flag (see -help for all options) ----------------------------------------------------- External libraries (freely available with LGPL compatible licenses) are: MiniSat by Niklas Een and Niklas Sorensson Heaps by Jean-Christophe Filliatre You can replace default solver MiniSAT with PicoSAT developed by Armin Biere using "make PicoSAT=true" Lingeling developed by Armin Biere using "make LGL=true"
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.