SPASSWriter

java.lang.Object

org.tweetyproject.logics.ml.writer.SPASSWriter

public class SPASSWriter extends Object

This class prints single first-order modal 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:

Constructor Summary

Constructors

Constructor

Description

SPASSWriter()

Creates a new SPASSWriter.

SPASSWriter(Writer writer)

Creates a new SPASSWriter.
Method Summary

Modifier and Type

Method

Description

void

close()

Closes the underlying writer stream.

void

printProblem(MlBeliefSet kb, RelationalFormula formula)

Prints the contents of a SPASS problem file for a given knowledge base and a formula.

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details
- SPASSWriter
  
  public SPASSWriter(Writer writer)
  
  Creates a new SPASSWriter.
  
  Parameters:
  
  writer - Output is redirected to this writer.
- SPASSWriter
  
  public SPASSWriter()
  
  Creates a new SPASSWriter.
Method Details
- printProblem
  
  public void printProblem(MlBeliefSet kb, RelationalFormula formula) throws ParserException, IOException
  
  Prints the contents of a SPASS problem file for a given knowledge base and a formula.
  
  Parameters:
  
  kb - a knowledge base
  
  formula - a relational formula
  
  Throws:
  
  ParserException - if parsing fails
  
  IOException - if an IO issue occurs.
- close
  
  public void close() throws IOException
  
  Closes the underlying writer stream.
  If an I/O error occurs while closing the writer, an `IOException` is thrown.
  
  Throws:
  
  IOException - if an I/O error occurs while closing the writer.