net.sf.tweety.logics.ml.writer

Class SPASSWriter

java.lang.Object

net.sf.tweety.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:

net.sf.tweety.logics.ml.reasoner.SPASSMlReasoner

Constructor Summary

Constructors

Constructor and Description
SPASSWriter() Creates a new SPASSWriter.
SPASSWriter(Writer writer) Creates a new SPASSWriter.

Method Summary

Modifier and Type	Method and Description
void	close()
void	printProblem(ModalBeliefSet kb, net.sf.tweety.logics.commons.syntax.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

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

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 Detail

printProblem

public void printProblem(ModalBeliefSet kb,
                         net.sf.tweety.logics.commons.syntax.RelationalFormula formula)
                  throws net.sf.tweety.commons.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:

net.sf.tweety.commons.ParserException

IOException

close

public void close()
           throws IOException

Throws:

IOException