Documentation

LS-Lab · Jan 25, 2021 · da3ea56 · da3ea56
1 parent c14be19
commit da3ea56
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git a/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/UnifyUSCalculus.scala b/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/UnifyUSCalculus.scala
@@ -2310,19 +2310,20 @@ trait UnifyUSCalculus {
   }
 
 
-  /** Which matcher to use for which [[ProvableInfo]].
-    * [[AxiomInfo.unifier]] will be consulted:
+  /** Which unification matcher to use for which [[ProvableInfo]].
+    * [[AxiomInfo.unifier]] declaration will be consulted from @[[edu.cmu.cs.ls.keymaerax.btactics.macros.Axiom]] declarations:
     * - 'surjective: A formula is surjective iff rule US can instantiate it to any of its axiom schema instances,
     *   so those obtained by uniformly replacing program constant symbols by hybrid games and unit predicationals by formulas.
     *   If no arguments occur, so no function or predicate symbols or predicationals, then the axiom is surjective.
     *   UnitFunctional, UnitPredicational, ProgramConst etc. can still occur.
     *   Function or predicate symbols that occur in a context without any bound variables are exempt. For example [[Ax.testb]].
-    *   [[UniformMatcher]]
+    *   Using [[UniformMatcher]]
     * - 'linear: No symbol can occur twice in the shape.
     *   If a symbol does occur twice, it is assumed that the identical match is found in all use cases,
     *   which is a strong assumption and can lead to unpredictable behavior otherwise.
-    *   [[LinearMatcher]]
+    *   Using [[LinearMatcher]]
     * - 'surjlinear: Both 'surject and 'linear
+    *   Using [[UniformMatcher]] but [[LinearMatcher]] would be okay/
     * - 'surjlinearpretend: An axiom that pretends to be surjective and linear even if it isn't necessarily so.
     * - 'full: General unification [[UnificationMatch]] is the default fallback.
     * @see Andre Platzer. [[https://doi.org/10.1007/s10817-016-9385-1 A complete uniform substitution calculus for differential dynamic logic]]. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017. arXiv:1601.06183

diff --git a/keymaerax-macros/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/macros/Axiom.scala b/keymaerax-macros/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/macros/Axiom.scala
@@ -29,7 +29,7 @@ import AnnotationCommon._
   * @param conclusion Formula string displayed for axioms as html with unicode in the user interface
   *  For axioms with (non-position) inputs, the conclusion must mention each input.
   *  Sequent syntax is optionally supported:   A, B |- C, D
-  * @param unifier Which unifier to use for axiom: "surjective" or "linear" or "surjlinear" or "surjlinearpretend" or "full" [[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.matcherFor()]]
+  * @param unifier Which unifier to use for axiom: "surjective" or "linear" or "surjlinear" or "surjlinearpretend" or "full" [[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus#matcherFor(edu.cmu.cs.ls.keymaerax.btactics.macros.ProvableInfo)]]
   * @param displayLevel Where to show the axiom: "internal" (not on UI at all), "browse", "menu", "all" (on UI everywhere)
   * @param inputs Display inputs for axiom-with-input as type declarations, e.g., "C:Formula" for cut.
   *               Arguments are separated with ;; and allowed fresh variables are given in square brackets, for example