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.GtkGenericATP

Description

Generic Gtk GUI for automatic theorem provers.

Documentation

genericATPgui Source #

Arguments

:: (Show sentence, 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