Hets - the Heterogeneous Tool Set

Copyright(c) Thiemo Wiedemeyer, Uni Bremen 2009
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerraider@informatik.uni-bremen.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

GUI.GenericATP

Description

Generic GUI for automatic theorem provers. CPP between HTk and Gtk.

Synopsis

Documentation

genericATPgui

Arguments

:: (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.