Package com.articulate.sigma.trans

Class THFutil

java.lang.Object

com.articulate.sigma.trans.THFutil

public class THFutil
extends Object

Constructor Summary

Constructors

Constructor	Description
THFutil()

Method Summary

Modifier and Type	Method	Description
static List<String>	fixNegatedQuantifiers(List<String> lines)	Wraps THF/TFF negated quantifiers so that "~ ? [..] : ..." becomes "~( ? [..] : ...
static List<String>	preprocessTHFProof(List<String> lines)

Methods inherited from class java.lang.Object

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

Constructor Details

THFutil

public THFutil()

Method Details

preprocessTHFProof

public static List<String> preprocessTHFProof(List<String> lines)

fixNegatedQuantifiers

public static List<String> fixNegatedQuantifiers(List<String> lines)

Wraps THF/TFF negated quantifiers so that "~ ? [..] : ..." becomes "~( ? [..] : ... )". This matches the ANTLR parser's rule thf_unary_formula := '~' '(' thf_logic_formula ')'.