gapt.proofs.lk

Attributes

Companion: object
Source: Attributes.scala
Supertypes: trait Serializable

trait Product

trait Equals

class Object

trait Matchable

class Any
Show all

Companion: class
Source: Attributes.scala
Supertypes: trait Product

trait Mirror

class Object

trait Matchable

class Any
Self type: Attributes.type

Source: LKProof.scala
Supertypes: trait SequentProof[Formula, LKProof]

trait DagProof[LKProof]

trait Product

trait Equals

class Object

trait Matchable

class Any
Show all
Known subtypes: 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
Show all

Class that describes how LKProofs can be substituted.

preserveEigenvariables: If true, preserve eigenvariables and never change them. If false (the default), treat eigenvariables as variables bound by their strong quantifier inferences and perform capture-avoiding substitution.

Source: LKProofSubstitutable.scala
Supertypes: trait Substitutable[Substitution, LKProof, LKProof]

class Object

trait Matchable

class Any
Known subtypes: object LKProofSubstitutableDefault.type

Source: package.scala
Supertypes: class LKProofSubstitutable

trait Substitutable[Substitution, LKProof, LKProof]

class Object

trait Matchable

class Any
Self type: LKProofSubstitutableDefault.type

Source: LKRuleCreationException.scala
Supertypes: class Exception

class Throwable

trait Serializable

class Object

trait Matchable

class Any
Show all

Implementation of the visitor pattern for gapt.proofs.lk.LKProof. Proof transformations can implement this trait to reduce boilerplate code.

Source: LKVisitor.scala
Supertypes: class Object

trait Matchable

class Any
Known subtypes: class ProofSegmentInsertionVisitor

object pushEqualityInferencesToLeaves2.type

object CreateASchemaVersion.type

Source: package.scala
Supertypes: trait Replaceable[LKProof, LKProof]

class Object

trait Matchable

class Any
Self type: lkProofReplaceable.type