Package com.articulate.sigma.parsing

Class TPTPWriter

java.lang.Object

com.articulate.sigma.parsing.TPTPWriter

public class TPTPWriter
extends Object

Field Summary

Fields

Modifier and Type	Field	Description
static boolean	debug
Set<FormulaAST>	formulas

Constructor Summary

Constructors

Constructor	Description
TPTPWriter()

Method Summary

Modifier and Type	Method	Description
static void	main(String[] args)
static void	showHelp()
static void	translate(String[] args)
String	visitAndsent(com.articulate.sigma.parsing.SuokifParser.AndsentContext context)	andsent : '(' 'and' sentence sentence+ ')' ;
String	visitArgument(com.articulate.sigma.parsing.SuokifParser.ArgumentContext context)	argument : (sentence | term) ;
String	visitComment(com.articulate.sigma.parsing.SuokifParser.CommentContext context)
String	visitEqsent(com.articulate.sigma.parsing.SuokifParser.EqsentContext context)	eqsent : '(' 'equal' term term ')' ; argument : (sentence | term) ; term : (funterm | variable | string | number | FUNWORD | IDENTIFIER ) ;
String	visitExists(com.articulate.sigma.parsing.SuokifParser.ExistsContext context)	exists : '(' 'exists' '(' variable+ ')' sentence ')' ;
String	visitFile(com.articulate.sigma.parsing.SuokifParser.FileContext context)	file : (sentence | comment)+ EOF ;
String	visitForall(com.articulate.sigma.parsing.SuokifParser.ForallContext context)	forall : '(' 'forall' '(' variable+ ')' sentence ')' ;
String	visitFunterm(com.articulate.sigma.parsing.SuokifParser.FuntermContext context)	funterm : '(' FUNWORD argument+ ')' ;
String	visitIff(com.articulate.sigma.parsing.SuokifParser.IffContext context)	iff : '(' 'invalid input: '<'=>' sentence sentence ')' ;
String	visitImplies(com.articulate.sigma.parsing.SuokifParser.ImpliesContext context)	implies : '(' '=>' sentence sentence ')' ;
String	visitLogsent(com.articulate.sigma.parsing.SuokifParser.LogsentContext context)	logsent : (notsent | andsent | orsent | implies | iff | eqsent) ;
String	visitNotsent(com.articulate.sigma.parsing.SuokifParser.NotsentContext context)	notsent : '(' 'not' sentence ')' ;
String	visitNumber(com.articulate.sigma.parsing.SuokifParser.NumberContext context)
String	visitOrsent(com.articulate.sigma.parsing.SuokifParser.OrsentContext context)	orsent : '(' 'or' sentence sentence+ ')' ;
String	visitQuantsent(com.articulate.sigma.parsing.SuokifParser.QuantsentContext context)	quantsent : (forall | exists) ;
String	visitRelsent(com.articulate.sigma.parsing.SuokifParser.RelsentContext context)	relsent : ('(' IDENTIFIER argument+ ')') | ('(' variable argument+ ')') ; argument : (sentence | term) ; term : (funterm | variable | string | number | FUNWORD | IDENTIFIER ) ; Set the types of any variables that appear in an instance or subclass declaration
String	visitSentence(com.articulate.sigma.parsing.SuokifParser.SentenceContext context)	sentence : (relsent | logsent | quantsent | variable) ;
String	visitString(com.articulate.sigma.parsing.SuokifParser.StringContext context)
String	visitTerm(com.articulate.sigma.parsing.SuokifParser.TermContext context)	term : (funterm | variable | string | number | FUNWORD | IDENTIFIER ) ;
String	visitVariable(com.articulate.sigma.parsing.SuokifParser.VariableContext context)	variable : (REGVAR | ROWVAR) ;
String	wrappedMetaFormat(FormulaAST f)

Methods inherited from class java.lang.Object

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

Field Details

formulas

public Set<FormulaAST> formulas

debug

public static boolean debug

Constructor Details

TPTPWriter

public TPTPWriter()

Method Details

visitFile

public String visitFile(com.articulate.sigma.parsing.SuokifParser.FileContext context)

file : (sentence | comment)+ EOF ;

Returns:

a String of TPTP formulas

visitSentence

public String visitSentence(com.articulate.sigma.parsing.SuokifParser.SentenceContext context)

sentence : (relsent | logsent | quantsent | variable) ;

visitComment

public String visitComment(com.articulate.sigma.parsing.SuokifParser.CommentContext context)

visitRelsent

public String visitRelsent(com.articulate.sigma.parsing.SuokifParser.RelsentContext context)

relsent : ('(' IDENTIFIER argument+ ')') | ('(' variable argument+ ')') ; argument : (sentence | term) ; term : (funterm | variable | string | number | FUNWORD | IDENTIFIER ) ; Set the types of any variables that appear in an instance or subclass declaration

visitArgument

public String visitArgument(com.articulate.sigma.parsing.SuokifParser.ArgumentContext context)

argument : (sentence | term) ;

visitLogsent

public String visitLogsent(com.articulate.sigma.parsing.SuokifParser.LogsentContext context)

logsent : (notsent | andsent | orsent | implies | iff | eqsent) ;

visitNotsent

public String visitNotsent(com.articulate.sigma.parsing.SuokifParser.NotsentContext context)

notsent : '(' 'not' sentence ')' ;

visitAndsent

public String visitAndsent(com.articulate.sigma.parsing.SuokifParser.AndsentContext context)

andsent : '(' 'and' sentence sentence+ ')' ;

visitOrsent

public String visitOrsent(com.articulate.sigma.parsing.SuokifParser.OrsentContext context)

orsent : '(' 'or' sentence sentence+ ')' ;

visitImplies

public String visitImplies(com.articulate.sigma.parsing.SuokifParser.ImpliesContext context)

implies : '(' '=>' sentence sentence ')' ;

visitIff

public String visitIff(com.articulate.sigma.parsing.SuokifParser.IffContext context)

iff : '(' 'invalid input: '<'=>' sentence sentence ')' ;

visitEqsent

public String visitEqsent(com.articulate.sigma.parsing.SuokifParser.EqsentContext context)

eqsent : '(' 'equal' term term ')' ; argument : (sentence | term) ; term : (funterm | variable | string | number | FUNWORD | IDENTIFIER ) ;

visitQuantsent

public String visitQuantsent(com.articulate.sigma.parsing.SuokifParser.QuantsentContext context)

quantsent : (forall | exists) ;

visitForall

public String visitForall(com.articulate.sigma.parsing.SuokifParser.ForallContext context)

forall : '(' 'forall' '(' variable+ ')' sentence ')' ;

visitExists

public String visitExists(com.articulate.sigma.parsing.SuokifParser.ExistsContext context)

exists : '(' 'exists' '(' variable+ ')' sentence ')' ;

visitVariable

public String visitVariable(com.articulate.sigma.parsing.SuokifParser.VariableContext context)

variable : (REGVAR | ROWVAR) ;

visitTerm

public String visitTerm(com.articulate.sigma.parsing.SuokifParser.TermContext context)

term : (funterm | variable | string | number | FUNWORD | IDENTIFIER ) ;

visitFunterm

public String visitFunterm(com.articulate.sigma.parsing.SuokifParser.FuntermContext context)

funterm : '(' FUNWORD argument+ ')' ;

visitString

public String visitString(com.articulate.sigma.parsing.SuokifParser.StringContext context)

visitNumber

public String visitNumber(com.articulate.sigma.parsing.SuokifParser.NumberContext context)

wrappedMetaFormat

public String wrappedMetaFormat(FormulaAST f)

showHelp

public static void showHelp()

translate

public static void translate(String[] args)

main

public static void main(String[] args)