gapt-examples
API
Generated with
gapt-examples/gapt.examples/gapt.examples.sequence/AllQuantifiedConditionalAxiomHelper

AllQuantifiedConditionalAxiomHelper

gapt.examples.sequence.AllQuantifiedConditionalAxiomHelper
class AllQuantifiedConditionalAxiomHelper(variables: List[FOLVar], conditions: List[FOLAtom], consequence: FOLFormula)

Auxiliary structure to deal with axioms of the schema: Forall variables cond1 -> cond2 -> ... -> condn -> consequence |- ...

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any

Members list

Value members

Concrete methods

def apply(expressions: List[FOLTerm], p: LKProof): LKProof

Use axiom with given expressions in proof. Consequence of axiom must appear in current proof. Instantiated conditions will of course remain in the antecedent of the returned proof

Use axiom with given expressions in proof. Consequence of axiom must appear in current proof. Instantiated conditions will of course remain in the antecedent of the returned proof

Attributes

Concrete fields

val getAxiom: FOLFormula

Returns the full axiom

Returns the full axiom

Attributes

Generated with