Packages

package pt

Proof-term checker turns proof terms to proof certificates. edu.cmu.cs.ls.keymaerax.pt.ProofChecker turns a proof term to the edu.cmu.cs.ls.keymaerax.core.Provable that it proves.

ProofChecker : ProofTerm * Formula => Provable

This package defines

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. pt
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class AxiomTerm(name: String) extends ProofTerm with Product with Serializable
  2. case class BananaODE(sm: SymMode) extends SymMode with Product with Serializable
  3. case class ConSubst() extends SymMode with Product with Serializable
  4. case class ConversionException(msg: String) extends Exception with Product with Serializable
  5. case class Defun(sm: SymMode) extends SymMode with Product with Serializable
  6. case class DefunSubst() extends SymMode with Product with Serializable
  7. case class Depred(sm: SymMode) extends SymMode with Product with Serializable
  8. case class DepredSubst() extends SymMode with Product with Serializable
  9. case class ElidingProvable(provable: Provable, steps: Int, defs: Declaration) extends ProvableSig with Product with Serializable

    A direct Provable straight from the core that does not keep track of its proof term, but only tracks number of proof steps.

    A direct Provable straight from the core that does not keep track of its proof term, but only tracks number of proof steps. Directly forwards all function calls to provable.

  10. case class FOLRConstant(f: Formula) extends ProofTerm with Product with Serializable
  11. case class ForwardNewConsequenceTerm(child: ProofTerm, newConsequence: Sequent, rule: Rule) extends ProofTerm with Product with Serializable
  12. case class FunSubst() extends SymMode with Product with Serializable
  13. case class IAAllElim() extends Iaxiom with Product with Serializable
  14. case class IABoxSplit() extends Iaxiom with Product with Serializable
  15. case class IADC() extends Iaxiom with Product with Serializable
  16. case class IADE() extends Iaxiom with Product with Serializable
  17. case class IADG() extends Iaxiom with Product with Serializable
  18. case class IADIEq() extends Iaxiom with Product with Serializable
  19. case class IADS() extends Iaxiom with Product with Serializable
  20. case class IADW() extends Iaxiom with Product with Serializable
  21. case class IADiffEffectSys() extends Iaxiom with Product with Serializable
  22. case class IADiffLinear() extends Iaxiom with Product with Serializable
  23. case class IAEqualCommute() extends Iaxiom with Product with Serializable
  24. case class IAEquivReflexive() extends Iaxiom with Product with Serializable
  25. case class IAI() extends Iaxiom with Product with Serializable
  26. case class IAImpSelf() extends Iaxiom with Product with Serializable
  27. case class IAK() extends Iaxiom with Product with Serializable
  28. case class IAV() extends Iaxiom with Product with Serializable
  29. case class IAallInst() extends Iaxiom with Product with Serializable
  30. case class IAassign() extends Iaxiom with Product with Serializable
  31. case class IAassignEq() extends Iaxiom with Product with Serializable
  32. case class IAassignany() extends Iaxiom with Product with Serializable
  33. case class IAbox() extends Iaxiom with Product with Serializable
  34. case class IAchoice() extends Iaxiom with Product with Serializable
  35. case class IAcompose() extends Iaxiom with Product with Serializable
  36. case class IAconstFcong() extends Iaxiom with Product with Serializable
  37. case class IAdConst() extends Iaxiom with Product with Serializable
  38. case class IAdMinus() extends Iaxiom with Product with Serializable
  39. case class IAdMult() extends Iaxiom with Product with Serializable
  40. case class IAdPlus() extends Iaxiom with Product with Serializable
  41. case class IAdassign() extends Iaxiom with Product with Serializable
  42. case class IAdvar() extends Iaxiom with Product with Serializable
  43. case class IAllSpace() extends Ispace with Product with Serializable
  44. case class IAloopIter() extends Iaxiom with Product with Serializable
  45. case class IAnd(left: Iformula, right: Iformula) extends Iformula with Product with Serializable
  46. case class IAndL() extends Ilrule with Product with Serializable
  47. case class IAndR() extends Irrule with Product with Serializable
  48. case class IApplyLrule(r: Ilrule, i: Int) extends IruleApp with Product with Serializable
  49. case class IApplyRrule(r: Irrule, i: Int) extends IruleApp with Product with Serializable
  50. case class IAssign(id: ID, t: Itrm) extends Ihp with Product with Serializable
  51. case class IAssignRand(id: ID) extends Ihp with Product with Serializable
  52. case class IAtest() extends Iaxiom with Product with Serializable
  53. case class IAx(ax: Iaxiom) extends Ipt with Product with Serializable
  54. case class IAxRule(ar: IaxiomaticRule) extends Ipt with Product with Serializable
  55. case class IBRenameL(what: ID, repl: ID) extends Ilrule with Product with Serializable
  56. case class IBRenameR(what: ID, repl: ID) extends Irrule with Product with Serializable
  57. case class ICE() extends IaxiomaticRule with Product with Serializable
  58. case class ICQ() extends IaxiomaticRule with Product with Serializable
  59. case class ICT() extends IaxiomaticRule with Product with Serializable
  60. case class IChoice(left: Ihp, right: Ihp) extends Ihp with Product with Serializable
  61. case class ICloseId(i: Int, j: Int) extends IruleApp with Product with Serializable
  62. case class ICohide2(i: Int, j: Int) extends IruleApp with Product with Serializable
  63. case class ICohideR() extends Irrule with Product with Serializable
  64. case class ICohideRR() extends Irrule with Product with Serializable
  65. case class ICommuteEquivR() extends Irrule with Product with Serializable
  66. case class IConst(int: Int, sm: SymMode = NonSubst()) extends Itrm with Product with Serializable
  67. case class ICut(f: Iformula) extends IruleApp with Product with Serializable
  68. case class ICutLeft(f: Iformula) extends Ilrule with Product with Serializable
  69. case class ICutRight(f: Iformula) extends Irrule with Product with Serializable
  70. case class IDIGeqSchema(o: IODE, t1: Itrm, t2: Itrm) extends IruleApp with Product with Serializable
  71. case class IDMap(varMap: Map[(String, Option[Int]), String], funMap: Map[Either[String, String], String], predMap: Map[String, String], conMap: Map[Either[String, String], String], progMap: Map[String, String], odeMap: Map[String, String], fArity: Int, pArity: Int, maxVar: Int, maxFun: Int, maxPred: Int, maxCon: Int, maxProg: Int, maxOde: Int) extends Product with Serializable
  72. case class IDiamond(prog: Ihp, post: Iformula) extends Iformula with Product with Serializable
  73. case class IDiffAssign(id: ID, t: Itrm) extends Ihp with Product with Serializable
  74. case class IDiffVar(id: ID) extends Itrm with Product with Serializable
  75. case class IDifferential(child: Itrm) extends Itrm with Product with Serializable
  76. case class IEquivBackwardL() extends Ilrule with Product with Serializable
  77. case class IEquivForwardL() extends Ilrule with Product with Serializable
  78. case class IEquivL() extends Ilrule with Product with Serializable
  79. case class IEquivR() extends Irrule with Product with Serializable
  80. case class IEquivifyR() extends Irrule with Product with Serializable
  81. case class IEvolveODE(ode: IODE, con: Iformula) extends Ihp with Product with Serializable
  82. case class IExists(x: ID, child: Iformula) extends Iformula with Product with Serializable
  83. case class IFNC(child: Ipt, seq: Isequent, ra: IruleApp) extends Ipt with Product with Serializable
  84. case class IFOLRConstant(f: Iformula) extends Ipt with Product with Serializable
  85. case class IFunction(f: ID, args: List[Itrm]) extends Itrm with Product with Serializable
  86. case class IFunctional(f: ID) extends Itrm with Product with Serializable
  87. case class IG() extends IaxiomaticRule with Product with Serializable
  88. case class IGeq(left: Itrm, right: Itrm) extends Iformula with Product with Serializable
  89. case class IHideL() extends Ilrule with Product with Serializable
  90. case class IHideR() extends Irrule with Product with Serializable
  91. case class IImplyL() extends Ilrule with Product with Serializable
  92. case class IImplyR() extends Irrule with Product with Serializable
  93. case class IInContext(id: ID, child: Iformula) extends Iformula with Product with Serializable
  94. case class ILoop(child: Ihp) extends Ihp with Product with Serializable
  95. case class INBSpace(id: String) extends Ispace with Product with Serializable
  96. case class INot(child: Iformula) extends Iformula with Product with Serializable
  97. case class INotL() extends Ilrule with Product with Serializable
  98. sealed trait IODE extends AnyRef
  99. case class IOProd(left: IODE, right: IODE) extends IODE with Product with Serializable
  100. case class IOSing(x: ID, t: Itrm) extends IODE with Product with Serializable
  101. case class IOVar(id: ID, sp: Ispace) extends IODE with Product with Serializable
  102. case class IPlus(left: Itrm, right: Itrm) extends Itrm with Product with Serializable
  103. case class IPrUSubst(child: Ipt, sub: Isubst) extends Ipt with Product with Serializable
  104. case class IPro(child: Ipt, pro: Ipt) extends Ipt with Product with Serializable
  105. case class IProp(id: ID, args: List[Itrm]) extends Iformula with Product with Serializable
  106. case class IPvar(id: ID) extends Ihp with Product with Serializable
  107. case class IRuleApplication(child: Ipt, ra: IruleApp, branch: Int) extends Ipt with Product with Serializable
  108. case class ISequence(left: Ihp, right: Ihp) extends Ihp with Product with Serializable
  109. case class ISkolem() extends Irrule with Product with Serializable
  110. case class IStart(seq: Isequent) extends Ipt with Product with Serializable
  111. case class ISub(child: Ipt, sub: Ipt, branch: Int) extends Ipt with Product with Serializable
  112. case class ITest(child: Iformula) extends Ihp with Product with Serializable
  113. case class ITimes(left: Itrm, right: Itrm) extends Itrm with Product with Serializable
  114. case class ITrueR() extends Irrule with Product with Serializable
  115. case class IURename(what: ID, repl: ID) extends IruleApp with Product with Serializable
  116. case class IVar(id: ID) extends Itrm with Product with Serializable
  117. sealed trait Iaxiom extends AnyRef
  118. sealed trait IaxiomaticRule extends AnyRef
  119. sealed trait Iformula extends AnyRef
  120. sealed trait Ihp extends AnyRef
  121. sealed trait Ilrule extends AnyRef
  122. case class Imonb() extends IaxiomaticRule with Product with Serializable
  123. sealed trait Ipt extends AnyRef
  124. sealed trait Irrule extends AnyRef
  125. sealed trait IruleApp extends AnyRef
  126. class IsabelleConverter extends Logging
  127. sealed trait Ispace extends AnyRef
  128. case class Isubst(SFunctions: List[Option[Itrm]], SFuncls: List[Option[Itrm]], SPredicates: List[Option[Iformula]], SContexts: List[Option[Iformula]], SPrograms: List[Option[Ihp]], SODEs: List[Option[IODE]], SSpace: Ispace) extends Product with Serializable
  129. sealed trait Itrm extends AnyRef
  130. case class NonSubst() extends SymMode with Product with Serializable
  131. case class ProlongationTerm(child: ProofTerm, prolongation: ProofTerm) extends ProofTerm with Product with Serializable
  132. sealed abstract class ProofTerm extends AnyRef

    A Proof Term is a syntactic internalization of a proof of a differential dynamic logic theorem.

    A Proof Term is a syntactic internalization of a proof of a differential dynamic logic theorem. Proof Terms can be converted to Provables by the ProofChecker. Created by nfulton on 10/15/15.

    See also

    ProofChecker

  133. trait ProvableSig extends AnyRef

    A common signature for edu.cmu.cs.ls.keymaerax.pt.ProvableSig's and TermProvable's for use in the btactics package.

    A common signature for edu.cmu.cs.ls.keymaerax.pt.ProvableSig's and TermProvable's for use in the btactics package. This allows for tactics to construct proof terms or not depending on which implementation they use.

    This file mimics edu.cmu.cs.ls.keymaerax.core.Provable outside the core and forwards all operations to the core.

    See also

    Provable

  134. case class RuleApplication(child: ProofTerm, rule: Rule, subgoal: Int) extends ProofTerm with Product with Serializable

    Witness for rule application.

  135. case class RuleTerm(name: String) extends ProofTerm with Product with Serializable
  136. class ScalaBuilder extends SourceBuilder
  137. class SexpBuilder extends SourceBuilder
  138. abstract class SourceBuilder extends AnyRef
  139. case class StartProof(phi: Sequent) extends ProofTerm with Product with Serializable
  140. case class Sub(child: ProofTerm, sub: ProofTerm, idx: Int) extends ProofTerm with Product with Serializable
  141. sealed abstract class SymMode extends AnyRef
  142. case class TermProvable(provable: ProvableSig, pt: ProofTerm, defs: Declaration) extends ProvableSig with Logging with Product with Serializable

    TermProvable has the same signature as Provable, but constructs proof terms alongside Provables.

    TermProvable has the same signature as Provable, but constructs proof terms alongside Provables. The ProofTerms remember how the provable was proved.

  143. case class URenameTerm(child: ProofTerm, ren: URename) extends ProofTerm with Product with Serializable
  144. case class UsubstProvableTerm(child: ProofTerm, substitution: USubst) extends ProofTerm with Product with Serializable

Value Members

  1. object ElidingProvable extends Serializable
  2. object HOLConverter

    Converts kyx expressions to subset used by hol formalization.

    Converts kyx expressions to subset used by hol formalization. Just different enough from Isabelle syntax that it's not so easy to unify them just yet.

  3. object IDMap extends Logging with Serializable
  4. object Iaxiom extends Logging
  5. object IaxiomaticRule
  6. object IsabelleConverter extends Logging

    Convert proof terms to sublanguage + syntax used by Isabelle formalization Created by bbohrer on 10/19/17.

    Convert proof terms to sublanguage + syntax used by Isabelle formalization Created by bbohrer on 10/19/17.

    See also

    ProofChecker

  7. object NoProof extends ProofTerm with Product with Serializable
  8. object ProofChecker

    ProofChecker maps a proof term to the Provable it proves.

    ProofChecker maps a proof term to the Provable it proves.

    ProofChecker : ProofTerm * Formula => Provable

    with a successful answer if the proof indeed checked successfully. Not soundness-critical, because the proof checker compiles the proof term into subsequent proof rule and axiom applications in the prover core. Created by nfulton on 10/15/15.

    To do

    Currently not operational: fixme

    See also

    ProofTerm

    ProvableSig

  9. object ProvableSig

    See also

    Provable

  10. object TermProvable extends Serializable

Inherited from AnyRef

Inherited from Any

Ungrouped