gapt.examples.predicateEliminationProblems

Members list

Type members

Classlikes

object induction

Attributes

Supertypes
class Object
trait Matchable
class Any
Self type
induction.type

Attributes

Supertypes
class Object
trait Matchable
class Any
Self type

Value members

Concrete methods

def printResolutionCandidate(resolutionCandidate: PointedClause): Tree
def printSequent[T](sequent: Sequent[T]): Tree
def printer: PPrinter

Concrete fields

val badExample: ClauseSetPredicateEliminationProblem
val booleanUnification: PredicateEliminationProblem
val exampleRequiringSubsumption: ClauseSetPredicateEliminationProblem
val exampleRequiringTautologyDeletion: ClauseSetPredicateEliminationProblem
val exampleThatCanBeSolvedByPolarityRuleImmediately: ClauseSetPredicateEliminationProblem
val exampleThatUsesResolutionOnLiteralsThatAreNotQuantifiedVariables: ClauseSetPredicateEliminationProblem
val exampleWithQuantifiedVariableNotOccurring: ClauseSetPredicateEliminationProblem
val exampleWithSymmetryRequiringSubsumption: ClauseSetPredicateEliminationProblem
val exampleWithThreeClauses: ClauseSetPredicateEliminationProblem
val exampleWithTwoClauses: ClauseSetPredicateEliminationProblem
val exampleWithTwoVariables: ClauseSetPredicateEliminationProblem
val exampleWithoutQuantifiedVariables: ClauseSetPredicateEliminationProblem
val graphReachability: PredicateEliminationProblem
val negationOfLeibnizEquality: PredicateEliminationProblem
val negationOfModalAxiom: PredicateEliminationProblem
val onlyOneSidedClauses: ClauseSetPredicateEliminationProblem
val single2PartDisjunction: ClauseSetPredicateEliminationProblem
val single3PartDisjunction: ClauseSetPredicateEliminationProblem
val soqeBookDLSStarExample: ClauseSetPredicateEliminationProblem
val subsumptionByXLiteral: ClauseSetPredicateEliminationProblem
val twoStepRedundancy: ClauseSetPredicateEliminationProblem
val unsatisfiableExampleThatRequiresFactoring: ClauseSetPredicateEliminationProblem
val wernhardUnificationExample: ClauseSetPredicateEliminationProblem
val witnessBlowup: ClauseSetPredicateEliminationProblem