Pickrule
The pick* functions generalize the convenience constructors of the LK rules which allow to specify arguments by a formula instead of an index. Here we lookup fitting matches for the auxiliary formulas of each LK rule. In the case of LK, fitting is defined as equality of the formula. In the case of LKsk, it is equality of formulas and skolem symbols. An algorithm using pickrule is therefore easier to transfer to LKsk.
Attributes
- Source
- Utils.scala
- Graph
-
- Supertypes
-
class Objecttrait Matchableclass Any
- Self type
-
Pickrule.type
Members list
Type members
Types
Attributes
- Source
- Utils.scala
Value members
Concrete methods
picks one occurrences from the candidates s.t. formulas (if it exists) are identical
picks one occurrences from the candidates s.t. formulas (if it exists) are identical
Value parameters
- aux
-
an index into p.endSequent
- candidates
-
a list of candidate formulas to pick a match for aux
- p
-
the proof which is used as template
Attributes
- Returns
-
the index of a fitting formulas for aux
- Source
- Utils.scala
picks one occurrences from the candidates s.t. formulas (if it exists) are identical.
picks one occurrences from the candidates s.t. formulas (if it exists) are identical.
Attributes
- Returns
-
the index of a fitting formulas for aux
- Source
- Utils.scala
picks 1 occurrence from the same list s.t. ac1 != ac2, where formulas and skolem label agree
picks 1 occurrence from the same list s.t. ac1 != ac2, where formulas and skolem label agree
Attributes
- Returns
-
a pair of index and remaining candidates
- Source
- Utils.scala
picks 2 occurrences from the same list s.t. ac1 != ac2, where formulas and skolem label agree
picks 2 occurrences from the same list s.t. ac1 != ac2, where formulas and skolem label agree
Attributes
- Returns
-
a list with the indices of a fitting formulas for aux1 / aux2
- Source
- Utils.scala
picks 2 occurrences from the same list s.t. ac1 != ac2, where formulas and skolem label agree
picks 2 occurrences from the same list s.t. ac1 != ac2, where formulas and skolem label agree
Attributes
- Returns
-
a list with the indices of a fitting formulas for aux1 / aux2
- Source
- Utils.scala
For a rule p with parent sequents ps and auxiliary formulas aux, pick a fitting formula for each aux formula in the correct part of the sequent. E.g. if p is an implication right rule, aux(0) will be picked from the antecedent of ps(0) and aux(1) will be picked from the succedent of ps(0).
For a rule p with parent sequents ps and auxiliary formulas aux, pick a fitting formula for each aux formula in the correct part of the sequent. E.g. if p is an implication right rule, aux(0) will be picked from the antecedent of ps(0) and aux(1) will be picked from the succedent of ps(0).
Value parameters
- new_parents
-
The intended parents for p'
- old_aux
-
The indices of the auxiliary formulas in the parents
- old_parents
-
The parents of p.
- p
-
The proof which rule should be simulated, we assume we want to mirror the inference to create a similar proof p'
Attributes
- Returns
-
a list of indices in new_parents where the formulas match old_aux
- Source
- Utils.scala