net.sf.tweety.logics.fol.writer

Class SPASSWriter

java.lang.Object

net.sf.tweety.logics.fol.writer.SPASSWriter

public class SPASSWriter
extends java.lang.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:

net.sf.tweety.logics.SpassFolReasoner.reasoner.SPASS

Field Summary

Fields

Modifier and Type	Field and Description
(package private) java.io.Writer	writer Output is redirected to this writer.

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
void	close()
private java.lang.String	printDescription() Generates a generic description part for a SPASS problem file.
private java.lang.String	printFormula(RelationalFormula f)
private java.lang.String	printFormulas(FolBeliefSet kb, RelationalFormula formula) Prints the axioms declaration and conjectures declaration for a SPASS input file.
void	printProblem(FolBeliefSet kb, RelationalFormula formula) Prints the contents of a SPASS problem file for a given knowledge base and a formula.
private java.lang.String	printSignature(FolSignature signature) Prints the symbols declaration for a SPASS input file.

Methods inherited from class java.lang.Object

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

Field Detail

writer

final java.io.Writer writer

Output is redirected to this writer.

Constructor Detail

SPASSWriter

public SPASSWriter(java.io.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(FolBeliefSet kb,
                         RelationalFormula formula)
                  throws ParserException,
                         java.io.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

java.io.IOException

printDescription

private java.lang.String printDescription()

Generates a generic description part for a SPASS problem file.

Returns:

a string containing the description part

printSignature

private java.lang.String printSignature(FolSignature signature)

Prints the symbols declaration for a SPASS input file. First-order quantifiers and operators are do not need to be declared. All declared symbols have to be different from each other.

Parameters:

signature - FolSignature of the problem

Returns:

a string containing the signature declaration

printFormulas

private java.lang.String printFormulas(FolBeliefSet kb,
                                       RelationalFormula formula)

Prints the axioms declaration and conjectures declaration for a SPASS input file. All formulas must be closed.

Parameters:

kb - a knowledge base of relational formulas that will be used as the axioms declarations

formula - a formula that will be used as the conjectures declaration

Returns:

a string containing the axioms and conjectures declaration

See Also:

https://webspass.spass-prover.org/help/spass-input-syntax15.pdf

printFormula

private java.lang.String printFormula(RelationalFormula f)

close

public void close()
           throws java.io.IOException

Throws:

java.io.IOException