gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.reduction/PredicateTranslation

PredicateTranslation

gapt.proofs.reduction.PredicateTranslation
case class PredicateTranslation(context: Context)

Sets up the predicate reduction for first-order multi-sorted languages.

Value parameters

context

The context for which the predicate translation is to be constructed.

Attributes

Source
manySorted.scala
Graph
Supertypes
trait Serializable
trait Product
trait Equals
class Object
trait Matchable
class Any
Show all

Members list

Value members

Concrete methods

def guard(formula: Formula): Formula

Attributes

Source
manySorted.scala
def nonEmptyAxiom(s: TBase): Formula

Attributes

Source
manySorted.scala
def unguard(formula: Formula): Formula

Attributes

Source
manySorted.scala

Inherited methods

def productElementNames: Iterator[String]

Attributes

Inherited from:
Product
def productIterator: Iterator[Any]

Attributes

Inherited from:
Product

Concrete fields

val functionAxiom: Map[Const, Formula]

Attributes

Source
manySorted.scala
val nonEmptyAxioms: Set[Formula]

Attributes

Source
manySorted.scala
val predicateAxioms: Set[Formula]

Attributes

Source
manySorted.scala
val predicates: Set[HOLAtomConst]

Attributes

Source
manySorted.scala
Generated with