jtp.proof
Class ProofUtil

java.lang.Object
  |
  +--jtp.proof.ProofUtil

public class ProofUtil

extends Object

Constructor Summary

ProofUtil()

Method Summary

static Object	deReferenceGoal(Object g)
static Set	getVars(Clause cl)
static Set	getVars(CNFSentence sent)
static Set	getVars(Literal lit)
static Set	getVars(Object o)
static CNFSentence	instantiate(CNFSentence sent, Map bindings)
static Literal	instantiate(Literal litIn, Map bindings)
static List	invertPolarity(List literals)
static String	prefixify(String s, String prefix) Inserts the prefix at the beginning of every line in s
static String	prettyPrintGoal(Object goal, String prefix)
static String	printClauseAsImplication(Clause c, String prefix)
static String	printLiteral(Literal l, boolean flip)
static Proof	simplify(Proof p)
static CNFSentence	toConjunction(List conj)
static Implication	toImplication(CNFSentence s)

Methods inherited from class java.lang.Object

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

Constructor Detail

ProofUtil

public ProofUtil()

Method Detail

toImplication

public static Implication toImplication(CNFSentence s)
                                 throws ImplicationConversionException

ImplicationConversionException

invertPolarity

public static List invertPolarity(List literals)

deReferenceGoal

public static Object deReferenceGoal(Object g)

prettyPrintGoal

public static String prettyPrintGoal(Object goal,
                                     String prefix)

prefixify

public static String prefixify(String s,
                               String prefix)

Inserts the prefix at the beginning of every line in s

printClauseAsImplication

public static String printClauseAsImplication(Clause c,
                                              String prefix)

printLiteral

public static String printLiteral(Literal l,
                                  boolean flip)

instantiate

public static CNFSentence instantiate(CNFSentence sent,
                                      Map bindings)

instantiate

public static Literal instantiate(Literal litIn,
                                  Map bindings)

simplify

public static Proof simplify(Proof p)

toConjunction

public static CNFSentence toConjunction(List conj)

getVars

public static Set getVars(Object o)

getVars

public static Set getVars(CNFSentence sent)

getVars

public static Set getVars(Clause cl)

getVars

public static Set getVars(Literal lit)