Hets - the Heterogeneous Tool Set

Copyright(c) Rene Wagner, Heng Jiang, Uni Bremen 2007
LicenseGPLv2 or higher, see LICENSE.txt
Safe HaskellSafe-Inferred




Data structures representing SPASS signatures. Refer to http://spass.mpi-sb.mpg.de/webspass/help/syntax/dfgsyntax.html for the SPASS syntax documentation.


Externally used data structures

type SoftFOLMorphism = DefaultMorphism Sign

We use the DefaultMorphism for SPASS.

data Sign

This Signature data type will be translated to the SoftFOL data types internally.

sortRel contains the sorts relation. For each sort we need to know if it is a generated sort and if so by which functions it is possibly freely generated (sortMap).

For each function the types of all arguments and the return type must be known (funcMap). The same goes for the arguments of a predicate (predMap).

data Generated

Sorts can be (freely) generated by a set of functions.



emptySign :: Sign

Creates an empty Signature.

type Sentence = SPTerm

A Sentence is a SoftFOL Term.

type SPIdentifier = Token

A SPASS Identifier is a String for now.

singleSortNotGen :: Sign -> Bool

Check a Sign if it is single sorted (and the sort is non-generated).

Symbol related datatypes

Internal data structures

SPASS Problems

data SPProblem

A SPASS problem consists of a description and a logical part. The optional settings part hasn't been implemented yet.


Eq SPProblem 
Data SPProblem 
Ord SPProblem 
Show SPProblem 
ShATermConvertible SPProblem 
Pretty SPProblem

Creates a Doc from a SPASS Problem.

PrintTPTP SPProblem

Creates a Doc from a SoftFOL Problem.

Typeable * SPProblem 

SPASS Logical Parts

data SPLogicalPart

A SPASS logical part consists of a symbol list, a declaration list, and a set of formula lists. Support for clause lists and proof lists hasn't been implemented yet.


Symbol Lists

data SPSymbolList

All non-predefined signature symbols must be declared as part of a SPASS symbol list.



emptySymbolList :: SPSymbolList

Creates an empty SPASS Symbol List.

data SPSignSym

A common data type used for all signature symbols.


Eq SPSignSym 
Data SPSignSym 
Ord SPSignSym 
Show SPSignSym 
ShATermConvertible SPSignSym 
Pretty SPSignSym

Helper function. Creates a Doc from a Signature Symbol.

Typeable * SPSignSym 


data SPDeclaration

SPASS Declarations allow the introduction of sorts.


Eq SPDeclaration 
Data SPDeclaration 
Ord SPDeclaration 
Show SPDeclaration 
ShATermConvertible SPDeclaration 
Pretty SPDeclaration

Creates a Doc from a SPASS Declaration

PrintTPTP SPDeclaration

Creates a Doc from a SoftFOL Declaration. A subsort declaration will be rewritten as a special SPQuantTerm.

Typeable * SPDeclaration 

Formula List

data SPFormulaList

SPASS Formula List


isAxiomFormula :: SPFormulaList -> Bool

test the origin type of the formula list

Clause List

data SPOriginType

There are axiom formulae and conjecture formulae.


Eq SPOriginType 
Data SPOriginType 
Ord SPOriginType 
Show SPOriginType 
ShATermConvertible SPOriginType 
Pretty SPOriginType

Creates a Doc from a SPASS Origin Type

PrintTPTP SPOriginType

Creates a Doc from a SoftFOL Origin Type.

Typeable * SPOriginType 

data Name


Name String 

data Info


Info [GenTerm] 

data SPLiteral

Literals for SPASS CNF and DNF (the boolean indicates a negated literal).


SPLiteral Bool SPSymbol 

data SPQuantSym

SPASS Quantifier Symbols.


Eq SPQuantSym 
Data SPQuantSym 
Ord SPQuantSym 
Show SPQuantSym 
ShATermConvertible SPQuantSym 
Pretty SPQuantSym

Creates a Doc from a SPASS Quantifier Symbol.

PrintTPTP SPQuantSym

Creates a Doc from a SoftFOL Quantifier Symbol.

Typeable * SPQuantSym 

data SPSymbol

SPASS Symbols.


Eq SPSymbol 
Data SPSymbol 
Ord SPSymbol 
Show SPSymbol 
ShATermConvertible SPSymbol 
Pretty SPSymbol

Creates a Doc from a SPASS Symbol. printSymbol :: SPSymbol-> Doc

PrintTPTP SPSymbol

Creates a Doc from a SoftFOL Symbol.

Typeable * SPSymbol 

Proof List

Formulae And Terms

type SPFormula = Named SPTerm

A SPASS Formula is modelled as a Named SPTerm for now. This doesn't reflect the fact that the SPASS syntax lists both term and label as optional.

helpers for generating SoftFOL formulas



:: SPIdentifier

Variable symbol: v

-> SPIdentifier

Sort symbol: s

-> SPTerm

Term: s(v)

SPASS Desciptions

data SPDescription

A description is mandatory for a SPASS problem. It has to specify at least a name, the name of the author, the status (see also SPLogState below), and a (verbose) description.


data SPLogState

The state of a SPASS problem can be satisfiable, unsatisfiable, or unknown.

SPASS Settings

data SPSetting

New impelmentation of Settings. See spass input syntax Version 1.5.


A Tupel of the Clause Relation



negateSentence :: SPTerm -> Maybe SPTerm

negate a sentence