Class SPASSWriter

java.lang.Object
org.tweetyproject.logics.fol.writer.SPASSWriter

public class SPASSWriter extends Object
This class prints single first-order logic formulas and knowledge bases to the SPASS format.

A SPASS input file consists of the following parts:

  • Description: Contains meta-information about the problem, i.e. name, author, satisfiability
  • Symbols: Signature declaration
  • Axioms: a list of formulas
  • Conjectures: a list of formulas
SPASS attempts to prove that the conjunction of all axioms implies the disjunction of all conjectures.
Author:
Anna Gessler
See Also: