SequentProof

gapt.proofs.SequentProof

trait SequentProof[+Formula, This <: SequentProof[Formula, This]] extends DagProof[This]

Attributes

Source: SequentProof.scala
Graph
Supertypes: trait DagProof[This]

trait Product

trait Equals

class Object

trait Matchable

class Any
Show all
Known subtypes: trait IvyResolutionProof

class Flip

class InitialClause

class Instantiate

class NewSymbol

class Paramodulation

class Propositional

class Resolution

class LKProof

class BinaryLKProof

class AndRightRule

class CutRule

class ImpLeftRule

class OrLeftRule

trait CommonRule

class AndLeftRule

class ContractionRule

class ContractionLeftRule

class ContractionRightRule

class ConversionRule

class ConversionLeftRule

class ConversionRightRule

class EqualityRule

class EqualityLeftRule

class EqualityRightRule

class ImpRightRule

class InductionRule

class NegLeftRule

class NegRightRule

class OrRightRule

trait SkolemQuantifierRule

class ExistsSkLeftRule

class ForallSkRightRule

class StrongQuantifierRule

class ExistsLeftRule

class ForallRightRule

class WeakQuantifierRule

class ExistsRightRule

class ForallLeftRule

class WeakeningLeftRule

class WeakeningRightRule

class InitialSequent

class OpenAssumption

object BottomAxiom.type

class LogicalAxiom

class ProofLink

class ReflexivityAxiom

object TopAxiom.type

class UnaryLKProof

class NDProof

class BinaryNDProof

class AndIntroRule

class EqualityElimRule

class ExcludedMiddleRule

class ExistsElimRule

class ImpElimRule

class NegElimRule

trait CommonRule

class AndElim1Rule

class AndElim2Rule

class BottomElimRule

class ContractionRule

class DefinitionRule

class ExistsIntroRule

class ForallElimRule

class ForallIntroRule

class ImpIntroRule

class InductionRule

class NegIntroRule

class OrElimRule

class OrIntro1Rule

class OrIntro2Rule

class WeakeningRule

class InitialSequent

class EqualityIntroRule

class LogicalAxiom

class TheoryAxiom

object TopIntroRule.type

class TernaryNDProof

class UnaryNDProof

trait ResolutionProof

class LocalResolutionRule

class AvatarContradiction

class AvatarSplit

class Factor

class InitialClause

class AvatarComponent

class Defn

class Input

class Refl

class Taut

class Paramod

class PropositionalResolutionRule

class AndL

class AndR1

class AndR2

class BottomR

class DefIntro

class Flip

class ImpL1

class ImpL2

class ImpR

class NegL

class NegR

class OrL1

class OrL2

class OrR

class SkolemQuantResolutionRule

class AllL

class ExR

class TopL

class WeakQuantResolutionRule

class AllR

class ExL

class Resolution

class Subst

trait RefutationSketch

class SketchAxiom

class SketchComponentElim

class SketchComponentIntro

class SketchInference

class SketchSplitCombine

trait ContextRule[Formula, This]
Show all
Self type: This

Members list

Value members

Abstract methods

A list of lists of SequentIndices denoting the auxiliary formula(s) of the rule. The first list contains the auxiliary formulas in the first premise and so on.

Attributes

Source: SequentProof.scala

The conclusion of the rule.

Attributes

Source: SequentProof.scala

A list of SequentIndices denoting the main formula(s) of the rule.

Attributes

Source: SequentProof.scala

A list of occurrence connectors, one for each immediate subproof.

Attributes

Source: SequentProof.scala

Concrete methods

A list of lists containing the auxiliary formulas of the rule. The first list constains the auxiliary formulas in the first premise and so on.

Attributes

Source: SequentProof.scala

The list of main formulas of the rule.

Attributes

Source: SequentProof.scala

The upper sequents of the rule.

Attributes

Source: SequentProof.scala

Attributes

Definition Classes: DagProof
Source: SequentProof.scala

Inherited methods

Attributes

Inherited from:: Equals

Operations that view the sub-proofs as a DAG, which ignore duplicate sub-proofs, see gapt.proofs.DagProof.DagLikeOps for a list.

Attributes

Inherited from:: DagProof
Source: DagProof.scala

Depth of the proof, which is the maximum length of a path you can take via immediateSubProofs.

Attributes

Inherited from:: DagProof
Source: DagProof.scala

Compares the receiver object (this) with the argument object (that) for equivalence.

Any implementation of this method should be an equivalence relation:

It is reflexive: for any instance x of type Any, x.equals(x) should return true.
It is symmetric: for any instances x and y of type Any, x.equals(y) should return true if and only if y.equals(x) returns true.
It is transitive: for any instances x, y, and z of type Any if x.equals(y) returns true and y.equals(z) returns true, then x.equals(z) should return true.

If you override this method, you should verify that your implementation remains an equivalence relation. Additionally, when overriding this method it is usually necessary to override hashCode to ensure that objects which are "equal" (o1.equals(o2) returns true) hash to the same scala.Int. (o1.hashCode.equals(o2.hashCode)).

Value parameters

that: the object to compare against this object for equality.

Attributes

Returns: true if the receiver object is equivalent to the argument; false otherwise.
Definition Classes: DagProof -> Equals -> Any
Inherited from:: DagProof
Source: DagProof.scala

The immediate subproofs of this rule.

Attributes

Inherited from:: DagProof
Source: DagProof.scala

The name of this rule (in words).

Attributes

Inherited from:: DagProof
Source: DagProof.scala

The name of this rule (in symbols).

Attributes

Inherited from:: DagProof
Source: DagProof.scala

Attributes

Inherited from:: Product

Attributes

Inherited from:: Product

Attributes

Inherited from:: Product

Attributes

Inherited from:: Product

Attributes

Inherited from:: Product

Attributes

Inherited from:: Product

Returns the subproof at the given position: p.subProofAt(Nil) is p itself; p.subProofAt(i :: is) is the ith subproof of p.subProofAt(is).

Attributes

Inherited from:: DagProof
Source: DagProof.scala

Set of all (transitive) sub-proofs including this.

Attributes

Inherited from:: DagProof
Source: DagProof.scala

Returns a string representation of the object.

The default representation is platform dependent.

Attributes

Returns: a string representation of the object.
Definition Classes: DagProof -> Any
Inherited from:: DagProof
Source: DagProof.scala

Operations that view the sub-proofs as a tree, see gapt.proofs.DagProof.TreeLikeOps for a list.

Attributes

Inherited from:: DagProof
Source: DagProof.scala

Inherited fields

Calculate a hash code value for the object.

The default hashing algorithm is platform dependent.

Note that it is allowed for two objects to have identical hash codes (o1.hashCode.equals(o2.hashCode)) yet not be equal (o1.equals(o2) returns false). A degenerate implementation could always return 0. However, it is required that if two objects are equal (o1.equals(o2) returns true) that they have identical hash codes (o1.hashCode.equals(o2.hashCode)). Therefore, when overriding this method, be sure to verify that the behavior is consistent with the equals method.

Attributes

Returns: the hash code value for this object.
Inherited from:: DagProof
Source: DagProof.scala

In this article

Generated with