class UniformMatcher extends UniformMatching
- Alphabetic
- By Inheritance
- UniformMatcher
- UniformMatching
- BaseMatcher
- Logging
- LazyLogging
- LoggerHolder
- Matcher
- Function2
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new UniformMatcher()
Type Members
-
type
Subst = RenUSubst
The (generalized) substitutions used for unification purposes
-
type
SubstRepl = (Expression, Expression)
A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.
A (generalized) substitution pair, which is either like a SubstitutionPair for uniform substitution or a pair of Variable for uniform renaming.
- Definition Classes
- Matcher
- See also
SubstitutionPair
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
-
def
Subst(subs: List[SubstRepl]): Subst
Create a (generalized) substitution from the given representation
subs.Create a (generalized) substitution from the given representation
subs.- Attributes
- protected
- Definition Classes
- UniformMatching → Matcher
-
def
SubstRepl(what: Expression, repl: Expression): SubstRepl
Create a (generalized) substitution pair.
Create a (generalized) substitution pair.
- Attributes
- protected
- Definition Classes
- Matcher
- See also
SubstitutionPair
-
def
apply(e1: Sequent, e2: Sequent): Subst
apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Definition Classes
- BaseMatcher → Matcher
- Exceptions thrown
UnificationExceptionifinputcannot be matched against the patternshape.
-
def
apply(e1: DifferentialProgram, e2: DifferentialProgram): Subst
apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Definition Classes
- BaseMatcher → Matcher
- Exceptions thrown
UnificationExceptionifinputcannot be matched against the patternshape.
-
def
apply(e1: Program, e2: Program): Subst
apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Definition Classes
- BaseMatcher → Matcher
- Exceptions thrown
UnificationExceptionifinputcannot be matched against the patternshape.
-
def
apply(e1: Formula, e2: Formula): Subst
apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Definition Classes
- BaseMatcher → Matcher
- Exceptions thrown
UnificationExceptionifinputcannot be matched against the patternshape.
-
def
apply(e1: Term, e2: Term): Subst
apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Definition Classes
- BaseMatcher → Matcher
- Exceptions thrown
UnificationExceptionifinputcannot be matched against the patternshape.
-
def
apply(e1: Expression, e2: Expression): Subst
apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.apply(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Definition Classes
- BaseMatcher → Matcher → Function2
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
coloredDotsTerm(s: Sort, color: Int = 1): Term
DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for non-Tuples
DotTerms of different "colors" for components of a Tuple, uncolored DotTerm for non-Tuples
- Definition Classes
- UniformMatching
coloredDotsTerm(Real) = • coloredDotsTerm(Real*Real) = (•_1, •_2) coloredDotsTerm(Real*Real*Real) = (•_1, •_2, •_3)
Example: -
def
curried: (Expression) ⇒ (Expression) ⇒ RenUSubst
- Definition Classes
- Function2
- Annotations
- @unspecialized()
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
val
id: List[SubstRepl]
Identity substitution
{}that does not change anything.Identity substitution
{}that does not change anything.- Attributes
- protected
- Definition Classes
- Matcher
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
join(s: List[SubstRepl], t: List[SubstRepl]): List[SubstRepl]
Union of renaming substitution representations:
join(s, t)gives the representation ofsperformed together witht, if compatible.Union of renaming substitution representations:
join(s, t)gives the representation ofsperformed together witht, if compatible.s \cup t = {p(.)~>F | (p(.)~>F) \in s} ++ {(p(.)~>F) | (p(.)~>F) \in t} if s and t are compatible, so do not map the same p(.) or f(.) or a to different replacements- returns
a substitution that has the same effect as applying both substitutions
sandtsimultaneously. Similar to returnings++tbut skipping duplicates and checking compatibility in passing.
- Attributes
- protected
- Definition Classes
- BaseMatcher
-
lazy val
logger: Logger
- Attributes
- protected
- Definition Classes
- LazyLogging → LoggerHolder
-
final
val
loggerName: String
- Attributes
- protected
- Definition Classes
- LoggerHolder
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- Function2 → AnyRef → Any
-
def
tupled: ((Expression, Expression)) ⇒ RenUSubst
- Definition Classes
- Function2
- Annotations
- @unspecialized()
-
def
unifiable(shape: Sequent, input: Sequent): Option[Subst]
unifiable(shape, input) Compute some unifier matching
inputagainst the patternshapeif unifiable else Noneunifiable(shape, input) Compute some unifier matching
inputagainst the patternshapeif unifiable else None- Definition Classes
- BaseMatcher → Matcher
-
def
unifiable(shape: Expression, input: Expression): Option[Subst]
unifiable(shape, input) Compute some unifier matching
inputagainst the patternshapeif unifiable else Noneunifiable(shape, input) Compute some unifier matching
inputagainst the patternshapeif unifiable else None- Definition Classes
- BaseMatcher → Matcher
-
def
unifier(e1: Sequent, e2: Sequent, us: List[SubstRepl]): Subst
Create the unifier
us(which was formed for e1 and e2, just for the record).Create the unifier
us(which was formed for e1 and e2, just for the record).- Attributes
- protected
- Definition Classes
- BaseMatcher
-
def
unifier(e1: Expression, e2: Expression, us: List[SubstRepl]): Subst
Create the unifier
us(which was formed for e1 and e2, just for the record).Create the unifier
us(which was formed for e1 and e2, just for the record).- Attributes
- protected
- Definition Classes
- BaseMatcher
-
def
unifier(shape: Expression, input: Expression): List[SubstRepl]
Construct the base unifier that forces
shapeandinputto unify unless equal alreadyConstruct the base unifier that forces
shapeandinputto unify unless equal already- returns
{shape~>input} unless shape=input in which case it's {}.
- Attributes
- protected
- Definition Classes
- BaseMatcher
-
def
unifies2(s1: Program, s2: Program, t1: Program, t2: Program): List[SubstRepl]
- Attributes
- protected
- Definition Classes
- UniformMatching
-
def
unifies2(s1: Formula, s2: Formula, t1: Formula, t2: Formula): List[SubstRepl]
- Attributes
- protected
- Definition Classes
- UniformMatching
-
def
unifies2(s1: Term, s2: Term, t1: Term, t2: Term): List[SubstRepl]
- Attributes
- protected
- Definition Classes
- UniformMatching
-
def
unifies2(s1: Expression, s2: Expression, t1: Expression, t2: Expression): List[SubstRepl]
unifies2(s1,s2, t1,t2)unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by sweeping uniform matching.unifies2(s1,s2, t1,t2)unifies the two expressions of shape (s2,s2) against the two inputs (t1,t2) by sweeping uniform matching.s1 = t1 | u1 s2 = t2 | u2 -------------------------------- provided u1 and u2 compatible (s1,s2) = (t1,t2) | u1 join u2
- Attributes
- protected
- Definition Classes
- UniformMatching
-
def
unifiesODE2(s1: DifferentialProgram, s2: DifferentialProgram, t1: DifferentialProgram, t2: DifferentialProgram): List[SubstRepl]
- Attributes
- protected
- Definition Classes
- UniformMatching
-
def
unify(s1: Sequent, s2: Sequent): List[SubstRepl]
unify(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.unify(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Attributes
- protected
- Definition Classes
- UniformMatcher → BaseMatcher
- Exceptions thrown
UnificationExceptionifinputcannot be matched against the patternshape.
-
def
unify(e1: Program, e2: Program): List[SubstRepl]
Algorithm for sweeping uniform matching.
Algorithm for sweeping uniform matching. unify(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Attributes
- protected
- Definition Classes
- UniformMatching → BaseMatcher
-
def
unify(e1: Formula, e2: Formula): List[SubstRepl]
Algorithm for sweeping uniform matching.
Algorithm for sweeping uniform matching. unify(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Attributes
- protected
- Definition Classes
- UniformMatching → BaseMatcher
-
def
unify(e1: Term, e2: Term): List[SubstRepl]
Algorithm for sweeping uniform matching.
Algorithm for sweeping uniform matching. unify(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Attributes
- protected
- Definition Classes
- UniformMatching → BaseMatcher
-
def
unify(shape: Expression, input: Expression): List[SubstRepl]
- Attributes
- protected
- Definition Classes
- BaseMatcher
-
def
unifyApplicationOf(F: (Function, Term) ⇒ Expression, f: Function, t: Term, e2: Expression): List[SubstRepl]
Unify
f(t)withe2whereFis the operator (FuncOforPredOf) that forms the ApplicationOff(t).Unify
f(t)withe2whereFis the operator (FuncOforPredOf) that forms the ApplicationOff(t).1) unify the argument
twith a DotTerm abstraction•(t may be a tuple, then•is a tuple: coloredDotsTerm)ua = unify(•, t)2) unifier = substitute with the inverse of the argument unifier e2f(•) ~> ua^-1(e2)- Attributes
- protected
- Definition Classes
- UniformMatching
given
t = (a, b),e2 = a2*b, therefore1)unify((•_1, •_2), (a, b))yieldsua = •_1 ~> a, •_2 ~> b2) the inverse isua-1 = a ~> •_1, b ~> •_2ua-1(e2) = •_12*•_2, resulting inf(•_1, •_2) ~> (•_1^2*•_2)the inverse substitution is applied top-down, i.e., larger abstractions get precedence when components oftoverlap:t = (x, y, x + y)ande2 = x + yyieldsf(•_1, •_2, •_3) ~> •_3; notf(•_1, •_2, •_3) ~> •_1 + •_2
Example: -
def
unifyODE(e1: DifferentialProgram, e2: DifferentialProgram): List[SubstRepl]
Algorithm for sweeping uniform matching.
Algorithm for sweeping uniform matching. unify(shape, input) matches
inputagainst the patternshapeto find a uniform substitution\resultsuch that\result(shape)==input.- Attributes
- protected
- Definition Classes
- UniformMatching → BaseMatcher
-
def
unifyVar(xp1: DifferentialSymbol, e2: Expression): List[SubstRepl]
unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.
unifyVar(x1',e2) gives a unifier making x1' equal to e2 unless it already is.
- returns
unifyVar(x1',x2')={x1~>x2} if x2' is a differential variable other than x1' unifyVar(x1',x1')={}
- Attributes
- protected
- Definition Classes
- UniformMatching
- Exceptions thrown
UnificationExceptionif e2 is not a differential variable
-
def
unifyVar(x1: Variable, e2: Expression): List[SubstRepl]
unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.
unifyVar(x1,e2) gives a unifier making x1 equal to e2 unless it already is.
- returns
unifyVar(x1,x2)={x1~>x2} if x2 is a variable other than x1. unifyVar(x1,x1)={}
- Attributes
- protected
- Definition Classes
- UniformMatching
- Exceptions thrown
UnificationExceptionif e2 is not a variable
-
def
ununifiable(shape: Sequent, input: Sequent): Nothing
Indicates that
inputcannot be matched against the patternshapeby raising a UnificationException.Indicates that
inputcannot be matched against the patternshapeby raising a UnificationException.- Attributes
- protected
- Definition Classes
- BaseMatcher
- Exceptions thrown
UnificationExceptionalways.
-
def
ununifiable(shape: Expression, input: Expression): Nothing
Indicates that
inputcannot be matched against the patternshapeby raising a UnificationException.Indicates that
inputcannot be matched against the patternshapeby raising a UnificationException.- Attributes
- protected
- Definition Classes
- BaseMatcher
- Exceptions thrown
UnificationExceptionalways.
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core- KeYmaera X kernel, proof certificates, main data structuresExpression- Differential dynamic logic expressions:Term,Formula,ProgramSequent- Sequents of formulasProvable- Proof certificates transformed by rules/axiomsRule- Proof rules as well asUSubstOnefor (one-pass) uniform substitutions and renaming.StaticSemantics- Static semantics with free and bound variable analysisKeYmaeraXParser.edu.cmu.cs.ls.keymaerax.parser- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser- Parser reading KeYmaera X model and proof archive.kyxfilesDLParser- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser- Combinator parser reading KeYmaera X model and proof archive.kyxfilesedu.cmu.cs.ls.keymaerax.infrastruct- Prover infrastructure outside the kernelUnificationMatch- Unification algorithmRenUSubst- Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context- Representation for contexts of formulas in which they occur.Augmentors- Augmenting formula and expression data structures with additional functionalityExpressionTraversal- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon- Bellerophon tactic language and tactic interpreterBelleExpr- Tactic language expressionsSequentialInterpreter- Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics- Bellerophon tactic library for conducting proofs.TactixLibrary- Main KeYmaera X tactic library including many proof tactics.HilbertCalculus- Hilbert Calculus for differential dynamic logicSequentCalculus- Sequent Calculus for propositional and first-order logicHybridProgramCalculus- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus- Unification-based uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]- Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma- Lemma mechanismLemma- Lemmas are Provables stored under a name, e.g., in files.LemmaDB- Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe- Real arithmetic back-end solversMathematicaQETool- Mathematica interface for real arithmetic.Z3QETool- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext- Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica- Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3- Z3 interface for real arithmetic including simplifiers.Entry Points
Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX- Command-line launcher for KeYmaera X supports command-line argument-helpto obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.AxIndex- Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex- Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax- Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos