Hets - the Heterogeneous Tool Set

Copyright(c) Rainer Grabbe
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

SoftFOL.ProverState

Contents

Description

Data structures and initialising functions for Prover state and configurations.

Synopsis

Data structures

SoftFOL specific functions for prover GUI

spassProverState

Arguments

:: Sign

SoftFOL signature

-> [Named SPTerm]

list of named SoftFOL terms containing axioms

-> [FreeDefMorphism SPTerm SoftFOLMorphism]

freeness constraints

-> SoftFOLProverState 

Creates an initial SoftFOL prover state with logical part.

insertSentenceGen

Arguments

:: SoftFOLProverState

prover state containing initial logical part

-> Named SPTerm

goal to add

-> SoftFOLProverState 

Inserts a named SoftFOL term into SoftFOL prover state.

showDFGProblem

Arguments

:: String

theory name

-> SoftFOLProverState

prover state containing initial logical part

-> Named SPTerm

goal to print

-> [String]

extra options

-> IO String

formatted output of the goal

Pretty printing SoftFOL goal in DFG format.

showTPTPProblemM

Arguments

:: String

theory name

-> SoftFOLProverState

prover state containing initial logical part

-> [String]

extra options

-> IO String

formatted output of the goal

Pretty printing SoftFOL-model-finding-problem in TPTP format.

showTPTPProblem

Arguments

:: String

theory name

-> SoftFOLProverState

prover state containing initial logical part

-> Named SPTerm

goal to print

-> [String]

extra options

-> IO String

formatted output of the goal

Pretty printing SoftFOL goal in TPTP format.

showTPTPProblemAux

Arguments

:: String

theory name

-> SoftFOLProverState

prover state containing initial logical part

-> Maybe (Named SPTerm)

possible goal to print

-> [String]

extra options

-> IO String

formatted output of the goal

parseSPASSCommands

Arguments

:: [String]

SPASS command line options

-> [SPSetting]

parsed parameters and options

Translates SPASS command line into [SPSetting]

getAxioms :: SoftFOLProverState -> [String]

get all axioms possibly used in a proof