Copyright | (c) Thiemo Wiedemeyer, Uni Bremen 2009 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | raider@informatik.uni-bremen.de |
Stability | provisional |
Portability | needs POSIX |
Safe Haskell | None |
Generic Gtk GUI for automatic theorem provers.
Documentation
:: (Ord proof_tree, Ord sentence) | |
=> ATPFunctions sign sentence mor proof_tree pst | prover specific functions |
-> Bool | prover supports extra options |
-> String | prover name |
-> String | theory name |
-> Theory sign sentence proof_tree | theory consisting of a signature and a list of Named sentence |
-> [FreeDefMorphism sentence mor] | freeness constraints |
-> proof_tree | initial empty proof_tree |
-> IO [ProofStatus proof_tree] | proof status for each goal |