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 GUI for automatic theorem provers. CPP between HTk and Gtk.
- genericATPgui :: (Ord proof_tree, Ord sentence) => ATPFunctions sign sentence mor proof_tree pst -> Bool -> String -> String -> Theory sign sentence proof_tree -> [FreeDefMorphism sentence mor] -> proof_tree -> IO [ProofStatus proof_tree]
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 |
Invokes the prover GUI. Users may start the batch prover run on all goals, or use a detailed GUI for proving each goal manually.