Class 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.
Anna Gessler
See Also:
  • Constructor Details

    • SPASSWriter

      public SPASSWriter(Writer writer)
      Creates a new SPASSWriter.
      writer - Output is redirected to this writer.
    • SPASSWriter

      public SPASSWriter()
      Creates a new SPASSWriter.
  • Method Details