Formulas

gapt.examples.Formulas
object Formulas

Contains some commonly used formulas.

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Self type
Formulas.type

Members list

Type members

Classlikes

object Peano

Contains definitions related to arithmetic.

Contains definitions related to arithmetic.

Attributes

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

Value members

Concrete methods

def CongBinaryEq(f: String): FOLFormula

Value parameters

f

A function symbol.

Attributes

Returns

A formula expressing that = is a congruence w.r.t. the binary function symbol f.

def CongUnaryEq(f: String): FOLFormula

Value parameters

f

A function symbol.

Attributes

Returns

A formula expressing that = is a congruence w.r.t. the unary function symbol f.

Concrete fields

val ReflexivityEq: FOLFormula

Attributes

Returns

A formula expressing the reflexivity of =.

val SymmetryEq: FOLFormula

Attributes

Returns

A formula expressing the symmetry of =.

val TransitivityEq: FOLFormula

Attributes

Returns

A formula expressing the transitivity of =.