gapt-examples
API
Generated with
gapt-examples/gapt.examples/gapt.examples.predicateEliminationProblems

gapt.examples.predicateEliminationProblems

package gapt.examples.predicateEliminationProblems

Members list

Type members

Classlikes

object induction

Attributes

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

Attributes

Supertypes
class Object
trait Matchable
class Any
Self type

Value members

Concrete methods

def inputSize(clauseSet: ClauseSetPredicateEliminationProblem): Int
def isWSOQEWitness(input: PredicateEliminationProblem, firstOrderEquivalent: FOLFormula, witness: Substitution): Boolean
def numberOfSymbols(expr: Expr): Int
def printResolutionCandidate(resolutionCandidate: PointedClause): Tree
def printSequent[T](sequent: Sequent[T]): Tree
def printer: PPrinter
def witnessSize(substitution: Substitution): Int
def wscanTest(): Unit
def wscanTestExample(example: ClauseSetPredicateEliminationProblem): (Option[Substitution], Long, Int, Option[Int])

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
Generated with