case class BetaCertificate(leftFormula: CertFormula, rightFormula: CertFormula, lemma: Boolean, _leftChild: Certificate, _rightChild: Certificate, _order: TermOrder) extends BinaryCertificate with Product with Serializable
Certificate corresponding to an application of beta rules with lemmas: the
rule describes the splitting of an antecedent formula
leftFormula | rightFormula into the cases
leftFormula and !leftFormula, rightFormula.
(If lemma is not set, the second case is just
rightFormula)
- Alphabetic
- By Inheritance
- BetaCertificate
- Serializable
- Product
- Equals
- BinaryCertificate
- Certificate
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new BetaCertificate(leftFormula: CertFormula, rightFormula: CertFormula, lemma: Boolean, _leftChild: Certificate, _rightChild: Certificate, _order: TermOrder)
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val _leftChild: Certificate
- val _order: TermOrder
- val _rightChild: Certificate
- def apply(i: Int): Certificate
- Definition Classes
- BinaryCertificate → Certificate
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- lazy val assumedFormulas: Set[CertFormula]
Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof).
Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof). We assume that all formulae live in the antecedent.
- Definition Classes
- Certificate
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- val closingConstraint: Conjunction
The constraint resulting from this proof
The constraint resulting from this proof
- Definition Classes
- BinaryCertificate → Certificate
- lazy val constants: Set[ConstantTerm]
Set of constants occurring in this certificate.
Set of constants occurring in this certificate. By default this will contain the set of all constants in sub-certificates, as well as constants in assumed formulas.
- Definition Classes
- Certificate
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val hashCode: Int
- Definition Classes
- BetaCertificate → AnyRef → Any
- lazy val inferenceCount: Int
- Definition Classes
- Certificate
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def iterator: Iterator[Certificate]
- Definition Classes
- BinaryCertificate → Certificate
- val leftChild: Certificate
- Definition Classes
- BinaryCertificate
- val leftFormula: CertFormula
- val lemma: Boolean
- def length: Int
- Definition Classes
- BinaryCertificate → Certificate
- val localAssumedFormulas: Set[CertFormula]
- Definition Classes
- BetaCertificate → Certificate
- val localBoundConstants: Set[ConstantTerm]
Constants bound by the root operator of the certificate.
Constants bound by the root operator of the certificate.
- Definition Classes
- Certificate
- val localProvidedFormulas: Seq[Set[CertFormula]]
Formulae that are introduced into the antecedent by this rule application (one set for each subproof).
Formulae that are introduced into the antecedent by this rule application (one set for each subproof). This will implicitly simplify formulae (all simplifications that are built into the datastructures are carried out).
- Definition Classes
- BetaCertificate → Certificate
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val order: TermOrder
- Definition Classes
- BinaryCertificate → Certificate
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- val rightChild: Certificate
- Definition Classes
- BinaryCertificate
- val rightFormula: CertFormula
- def size: Int
- Definition Classes
- Certificate
- def subCertificates: IndexedSeq[Certificate]
- Definition Classes
- Certificate
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- lazy val theoryAxioms: Set[CertFormula]
- Definition Classes
- Certificate
- def toString(): String
- Definition Classes
- BetaCertificate → AnyRef → Any
- def update(newSubCerts: Seq[Certificate], newLemma: Boolean): Certificate
- def update(newSubCerts: Seq[Certificate]): Certificate
- Definition Classes
- BetaCertificate → Certificate
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)