AcceptTac should never be used. It will just accept the current proof goal and will then put the next subgoal of the current proof on the goal stack or if there is none, it will convert the root proof goal to a theorem (without having proved it). Just use this tactic for preliminary putting a proof goal aside that should then be proved later.

AsmConjTac destructs a conjunction in the assumptions: \[ \begin{array}{c} \gamma_0,\ldots,\gamma_{i-1},\varphi\wedge\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\Phi \\\hline \gamma_0,\ldots,\gamma_{i-1},\varphi,\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\Phi \end{array} \]

AsmDisjTac makes a case split on a disjunction in the assumptions: \[ \begin{array}{c} \gamma_0,\ldots,\gamma_{i-1},\varphi\vee\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\Phi \\\hline \gamma_0,\ldots,\gamma_{i-1},\varphi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\Phi \hspace{5mm} \gamma_0,\ldots,\gamma_{i-1},\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\Phi \end{array} \]

AsmDropListTac removes the list of assumptions by repeatedly applying AsmDropTac.

AsmDropTac removes the assumption with the given index. \[ \begin{array}{c} \gamma_0,\ldots,\gamma_{n-1}\vdash\varphi \\\hline \gamma_0,\ldots,\gamma_{i-1},\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\varphi \end{array} \]

AsmInstNextTac takes the chosen assumption that must be of the form G phi and will add the new assumption phi derived from it using nxt next operators. \[ \begin{array}{c} \gamma_0,\ldots,\gamma_{i-1},\mathsf{G}\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\varphi \\\hline \mathsf{X}^{nxt}\psi,\gamma_0,\ldots,\gamma_{i-1},\mathsf{G}\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\varphi \end{array} \]

AsmInstTac takes the chosen assumption that must be of the form AG phi and will add the new assumption phi derived from it. \[ \begin{array}{c} \gamma_0,\ldots,\gamma_{i-1},\mathsf{G}\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\varphi \\\hline \psi,\gamma_0,\ldots,\gamma_{i-1},\mathsf{G}\psi,\gamma_{i+1},\ldots,\gamma_{n-1}\vdash\varphi \end{array} \]

AsmMpTac takes the chosen assumption that must be an implication, and applies the modus ponens to reduce the proof goal: \[ \begin{array}{c} \psi\to\varphi,\Gamma\vdash\varphi \\\hline \Gamma\vdash\psi \end{array} \]

AsmRewriteTac scans the assumptions for literals (possibly negated variables) and replaces them in the goal by either true or false

AsmSplitTac converts all assumptions into DNF and makes then case splits on all cubes of the DNF, where also the atoms of each cube are split into single assumptions.

AssumeInstThmTac similar to AssumeThmTac, this tactic also adds an already proved theorem to the assumptions of the goal. However, this tactic can be applied to a non-initial goal provided that the theorem is a safety property which is instantiated accordingly.

AssumeNextInstThmTac is similar to AssumeInstThmTac, this tactic also adds an already proved theorem to the assumptions of the goal. However, this tactic can be applied to a non-initial goal provided that the theorem is a safety property which is instantiated accordingly.

AssumeThmTac converts the theorem with the specified name to an implication that is added to the assumptions. Since all theorems refer to the initial point of time, this tactic can only be applied to initial goals.

AxiomTac checks whether the conclusion also occurs in the assumptions and if so, this subgoal is proven, and otherwise, it fails.

BoolCasesTac makes a case distinction on the given boolean expression: \[ \begin{array}{c} \Gamma\vdash\varphi \\\hline \neg\psi,\Gamma\vdash\varphi \hspace{5mm} \psi,\Gamma\vdash\varphi \end{array} \]

BoolListCasesTac makes a case distinction on the given list of boolean expressions. Since an exponential number of subgoals is generated, this tactic must be used with care, i.e., with small lists of expressions.

BootTac replaces all control-flow labels and variables with their initial values provided that the goal is an initial goal. Note that this tactic can only be applied to initial goals.

ConjLeftTac splits a conjunction into two subgoals: \[ \begin{array}{c} \Gamma\vdash\varphi\wedge\psi \\ \hline \Gamma\vdash\varphi \hspace{5mm} \varphi,\Gamma\vdash\psi \end{array} \]

ConjRightTac splits a conjunction into two subgoals: \[ \begin{array}{c} \Gamma\vdash\varphi\wedge\psi \\ \hline \Gamma\vdash\psi \hspace{5mm} \psi,\Gamma\vdash\varphi \end{array} \]

ConjTac splits a conjunction into two subgoals: \[ \begin{array}{c} \Gamma\vdash\varphi\wedge\psi \\ \hline \Gamma\vdash\varphi \hspace{5mm} \Gamma\vdash\psi \end{array} \]

ContraposTac applies the law of contraposition \[ \begin{array}{c} \Gamma\vdash\varphi\to\psi \\ \hline \Gamma\vdash\neg\psi\to\neg\varphi \end{array} \]

CutTac implements the well-known cut rule of sequent calculus. It can be understood as a tactic that first proves the given property as a lemma that is then used as an assumption to prove the current goal. \[ \begin{array}{c} \Gamma\vdash \varphi \\ \hline \Gamma\vdash \psi \hspace{5mm} \psi,\Gamma\vdash\varphi \end{array} \]

DischTac discharges an implication: \[ \begin{array}{c} \Gamma\vdash\varphi\to\psi \\ \hline \varphi,\Gamma\vdash\psi \end{array} \] It also works for negations (viewing them as implications): \[ \begin{array}{c} \Gamma\vdash\neg\varphi \\ \hline \varphi,\Gamma\vdash\mathsf{false} \end{array} \]

This tactic reduces a disjunction to its left part while using the negation of its right part as a further assumption: \[ \begin{array}{c} \Gamma\vdash\varphi\vee\psi\\\hline \neg\psi,\Gamma\vdash\varphi \end{array} \]

This tactic reduces a disjunction to its right part while using the negation of its left part as a further assumption: \[ \begin{array}{c} \Gamma\vdash\varphi\vee\psi\\\hline \neg\varphi,\Gamma\vdash\psi \end{array} \]

expand the current goal with the next assignments followed by repeated expansions with the now assignments until there are no further changes (caution: this may not terminate in case of causality conflicts)

expand the current goal with the immediate assignments of the system, i.e., with the abbreviations and the immediate assignments of the dataflow

expand the current goal with the next assignments of the system, using the next assignments of the control- and dataflow

expand the current goal with the immediate assignment whose name of the left hand side variable is given as argument

expand the current goal with the next assignments of the system, using the next assignments of the control- and dataflow

FairnessTac applies induction for proving fairness properties: \[ \begin{array}{c} \Gamma\vdash\mathsf{GF}\varphi\\ \hline \Gamma\vdash\mathsf{F}\varphi \hspace{5mm} \Gamma\vdash\mathsf{G}(\varphi\to\mathsf{XF}\varphi) \end{array} \]

GenTac removes universal path and time quantification which converts an initial goal to a universal goal: \[ \begin{array}{cc} \begin{array}{c} \Gamma\vdash \mathsf{A}\varphi\\ \hline \Gamma\vdash \varphi \end{array} & \begin{array}{c} \Gamma\vdash \mathsf{G}\varphi\\ \hline \Gamma\vdash \varphi \end{array} \end{array} \] Note that assumptions which refer to the current point of time have to be removed by this tactic.

IffTac replaces an equivalence to two implications: \[ \begin{array}{c} \Gamma\vdash \varphi\leftrightarrow\psi \\ \hline \Gamma\vdash\varphi\to\psi \hspace{5mm} \Gamma\vdash\psi\to\varphi \end{array} \]

ImpResTac searches for implications and equivalences in the assumptions and derives new assumptions as follows: \[ \begin{array}{cc} \begin{array}{c} \varphi,\varphi\to\psi,\Gamma\vdash\gamma \\\hline \varphi,\psi,\Gamma\vdash\gamma \end{array} & \begin{array}{c} \varphi,\varphi\leftrightarrow\psi,\Gamma\vdash\gamma \\\hline \varphi,\psi,\Gamma\vdash\gamma \end{array} \end{array} \]

InductInvTac applies temporal induction using an induction lemma \(\chi\): \[ \begin{array}{c} \Gamma\vdash \mathsf{G}\varphi \\ \hline \Gamma\vdash \chi \hspace{5mm} \Gamma\vdash \mathsf{G}(\chi\to\varphi\wedge\mathsf{X}\chi) \end{array} \]

InductTac applies temporal induction \[ \begin{array}{c} \Gamma\vdash \mathsf{G}\varphi \\ \hline \Gamma\vdash \varphi \hspace{5mm} \Gamma\vdash \mathsf{G}(\varphi\to\mathsf{X}\varphi) \end{array} \]

InductWeakBeforeInvTac implements induction for a Weak-Before formula using an induction lemma \(\chi\): \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{B}\;\psi] \\ \hline \Gamma\vdash\chi\hspace{5mm} \Gamma\vdash\mathsf{G}((\varphi\to\psi)\wedge\chi\to\neg\psi\wedge\mathsf{X}\chi) \end{array} \] The rule is correct and complete, i.e., we can always find a suitable invariant \(\chi\) to prove the goal. Moreover, note that \((\varphi\to\psi)\wedge\chi\to\neg\psi\wedge\mathsf{X}\chi\) is equivalent to \(\chi\to\neg\psi\wedge(\varphi\vee\mathsf{X}\chi)\) which is used in the translation to \(\omega\)-automata.

InductWeakBeforeTac implements induction for a Weak-Before formula using invariant \(\chi := \neg\psi\) in InductWeakBeforeInvTac: \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{B}\;\psi] \\ \hline \Gamma\vdash\neg\psi\hspace{5mm} \Gamma\vdash\mathsf{G}(\neg\varphi\wedge\neg\psi\to\mathsf{X}\neg\psi) \end{array} \] Note that the subgoals imply the root goal, but not vice versa!

InductWeakUntilInvTac implements induction for a Weak-Until formula using an induction lemma \(\chi\): \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{U}\;\psi] \\ \hline \Gamma\vdash\chi\hspace{5mm} \Gamma\vdash\mathsf{G}(\neg\psi\wedge\chi\to\varphi\wedge\mathsf{X}\chi) \end{array} \] The rule is correct and complete, i.e., we can always find a suitable invariant \(\chi\) to prove the goal. Moreover, note that \(\neg\psi\wedge\chi\to\varphi\wedge\mathsf{X}\chi\) is equivalent to \(\chi\to\psi\vee\varphi\wedge\mathsf{X}\chi\) which is used in the translation to \(\omega\)-automata.

InductWeakUntilTac implements induction for a Weak-Until formula using invariant \(\chi := \varphi\vee\psi\) in InductWeakUntilInvTac: \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{U}\;\psi] \\ \hline \Gamma\vdash\varphi\vee\psi\hspace{5mm} \Gamma\vdash\mathsf{G}(\varphi\wedge\neg\psi\to\mathsf{X}(\varphi\vee\psi)) \end{array} \] Note that the subgoals imply the root goal, but not vice versa since the \([\varphi\;\mathsf{U}\;\psi]\) may be satisfied by a prefix of a path while the induction step must always hold: If \(\psi\) holds first, then also \([\varphi\;\mathsf{U}\;\psi]\) holds, but if afterwards, we have \(\varphi\wedge\neg\psi\) and after that \(\neg\varphi\wedge\neg\psi\), then the induction step fails.

InductWeakWhenInvTac implements induction for a Weak-When formula using an induction lemma \(\chi\): \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{W}\;\psi] \\ \hline \Gamma\vdash\chi\hspace{5mm} \Gamma\vdash\mathsf{G}(\neg(\varphi\wedge\psi)\wedge\chi\to\neg\psi\wedge\mathsf{X}\chi) \end{array} \] The rule is correct and complete, i.e., we can always find a suitable invariant \(\chi\) to prove the goal. Moreover, note that \(\neg(\varphi\wedge\psi)\wedge\chi\to\neg\psi\wedge\mathsf{X}\chi\) is equivalent to \(\chi\to(\psi\to\varphi)\wedge(\neg\psi\to\mathsf{X}\chi)\) and also equivalent to \(\chi\to \varphi\wedge\psi \vee \neg\psi\wedge\mathsf{X}\chi\) which are used in the translation to \(\omega\)-automata.

InductWeakWhenTac implements induction for a Weak-When formula using invariant \(\chi := \psi\to\varphi\) in InductWeakWhenInvTac: \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{W}\;\psi] \\ \hline \Gamma\vdash\psi\to\varphi\hspace{5mm} \Gamma\vdash\mathsf{G}(\neg\psi\to\mathsf{X}(\psi\to\varphi)) \end{array} \] Note that the subgoals imply the root goal, but not vice versa!

check whether a given name is already used by some goal

LTL2DetOmegaTac translates a LTL formula to a deterministic automaton.

LTL2OmegaTac translates a LTL formula to a nondeterministic automaton. The translation computes a universal automaton, so that the transition relation becomes an assumption in form of a AG formula. Moreover, potential fairness constraints are also added as assumptions. The option tryFG is used to avoid fairness constraints as much as possible.

LTLTac proves the given goal by by abstracting it into a LTL formula where the abstraction is made for any atom which is not a boolean variable or a boolean expression

The tactic can be used to prove a liveness property by unrolling of the liveness property \(\psi\): \[ \begin{array}{c} \Gamma\vdash\mathsf{F}\psi\\ \hline \Gamma\vdash \psi\vee \mathsf{X}(\psi\vee \mathsf{X}(\ldots)) \end{array} \] This rule can be used if the liveness is guaranteed to hold in a finite bound on the number of steps where the bound must be independent of the inputs of the program.

The tactic can be used to prove a liveness property if the property holds at the next point in time: \[ \begin{array}{c} \Gamma\vdash\mathsf{F}\psi\\ \hline \Gamma\vdash \mathsf{X}\psi \end{array} \]

The tactic can be used to prove a liveness property by means of a ranking function which is defined by an tuple of nat expressions \(\varrho\) and an invariant \(\chi\) such that the invariant holds until and when the liveness property \(\psi\) holds, and such that the ranking function is strictly decreasing until \(\psi\) holds and \(\psi\) holds when \(\varrho\) becomes zero: \[ \begin{array}{c} \Gamma\vdash\mathsf{F}\psi\\ \hline \Gamma\vdash \chi \hspace{5mm} \Gamma\vdash \mathsf{G} (\chi \wedge \neg\psi \to \mathsf{next}(\varrho)<\varrho \wedge \mathsf{X} \chi) \end{array} \]

This tactic can prove a liveness property by a ranking sequence which is inspired by the iteration $\varphi_{i+1} := \mathsf{AX}\varphi_i$. However, due to abstract states, there may be pseudo-cycles so that the subgoals only demand $\varphi_{i+1}\to\mathsf{F}\varphi_i$ which allows one to prove the latter by disproving the existence of the pseudo-cycles: \[ \begin{array}{c} \Gamma\vdash \mathsf{G}\left(\psi\mathsf{F}\varphi_0\right)\\ \hline \Gamma\vdash \psi\to\bigvee_{j=0}^n\varphi_j \hspace{5mm} \bigwedge_{i=0}^{n-1}\Gamma\vdash \mathsf{G}(\varphi_{i+1}\to\mathsf{F}\bigvee_{j=0}^i\varphi_j) \end{array} \]

The tactic can be used to prove a liveness property by means of a ranking function which is defined by a tuple of nat expressions \(\varrho\) which is strictly decreasing until \(\psi\) holds: \[ \begin{array}{c} \Gamma\vdash\mathsf{F}\psi\\ \hline \Gamma\vdash[(\mathsf{next}(\varrho)<\varrho)\;\mathsf{U}\;\psi] \end{array} \]

generate a new proof context for a Quartz module loaded from a file

generate a new proof context for a Quartz module loaded from the internet

generate a new proof context for a Quartz module loaded from a stream

generate a new proof context for a Quartz module loaded from a string

MpTac applies the well-known logic rule of modus ponens which can be used to strengthen a proof goal: \[ \begin{array}{c} \Gamma\vdash \varphi \\ \hline \Gamma\vdash\psi \hspace{5mm} \Gamma\vdash\psi\to\varphi \end{array} \]

drive an outermost temporal next operator inwards to the atoms of its subformulas, and convert it to a BoolNext operator for expanding with transition equations

NoTac does nothing, but is useful with OrelseTac tac NoTac to catch failing tactics.

OrelseTac applies the first tactic, and uses the second one if that fails.

parsing an expression from a string using the variable declarations of the proof context

parsing a SpecExpr from a string using the variable declarations of the proof context

PersistenceTac proves persistence properties by a property \(\chi\) which is after the point of time where the properties becomes invariantly true: \[ \begin{array}{c} \Gamma\vdash\mathsf{FG}\varphi\\ \hline \Gamma\vdash\mathsf{F}\chi \hspace{5mm} \Gamma\vdash\mathsf{G}(\chi\to\mathsf{G}\varphi) \end{array} \]

print the topmost proof goal

print the root goal of the current (open) proof goal

print init equations

print now equations

print next (transition) equations

print all open proof goals

print the proof of an already proved theorem

print the proof tree of the current proof goal

print the proof tree below a node in the proof tree

print the tactic used so far for the given node in the proof tree

print the tactic of an already proved theorem

print all proved goals, i.e., the available theorems

This function uses argument phi to set a new initial goal without assumptions and applies the given tactic. If the tactic proves the goal, it will be converted to a theorem and will be stored under the given name. Using successful tactics, this function can be considered as a proof based on the used tactics.

This function uses argument phi to set a new initial goal with given assumptions and applies the given tactic. If the tactic proves the goal, it will be converted to a theorem and will be stored under the given name. Using successful tactics, this function can be considered as a proof based on the used tactics.

remove the current goal with all of its subgoals

RepeatTac applies the given tactic as long as there are changes.

reset the proof tree without changing the contained AIF system and the related substitutions

set a new proof goal with a name to store it later as a theorem

This tactic uses Microsoft's SMT solver Z3 to prove the proof goal. It expects a list of theorems of the form AG phi which are instantiated to the current point of time, and are then added to the assumptions for proving the goal with its assumptions. A counterexample is printed if the goal cannot be proved. In contrast to TautTac, this tactic can deal with arithmetic, i.e., proving that n+1==1+n.

 The tactic replaces a strong temporal logic operator on top of the goal
 by a conjunction with the corresponding weak temporal logic operator and
 a liveness constraint:
 \[
 \begin{array}{l}
 [\varphi\;\mathsf{\underline{B}}\;\psi] = 
      [\varphi\;\mathsf{B}\;\psi] \wedge (\mathsf{F}\phi)\\
 [\varphi\;\mathsf{\underline{U}}\;\psi] = 
      [\varphi\;\mathsf{U}\;\psi] \wedge (\mathsf{F}\psi)\\
 [\varphi\;\mathsf{\underline{W}}\;\psi] = 
      [\varphi\;\mathsf{W}\;\psi] \wedge (\mathsf{F}\psi)\\
 \end{array}
 \]

StrongBeforeTac reduces Strong-Before to Weak-Before and Eventual: \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{\underline{B}}\;\psi] \\ \hline \Gamma\vdash [\varphi\;\mathsf{B}\;\psi] \hspace{5mm} \Gamma\vdash\mathsf{F}\phi \end{array} \]

StrongUntilTac reduces Strong-Until to Weak-Until and Eventual: \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{\underline{U}}\;\psi] \\ \hline \Gamma\vdash [\varphi\;\mathsf{U}\;\psi] \hspace{5mm} \Gamma\vdash\mathsf{F}\psi \end{array} \]

StrongWhenTac reduces Strong-When to Weak-When and Eventual: \[ \begin{array}{c} \Gamma\vdash [\varphi\;\mathsf{\underline{W}}\;\psi] \\ \hline \Gamma\vdash [\varphi\;\mathsf{W}\;\psi] \hspace{5mm} \Gamma\vdash\mathsf{F}\psi \end{array} \]

This tactic uses Microsoft's SMT solver Z3 to prove the proof goal. It expects a list of theorems of the form AG phi which are instantiated to the current point of time, and are then added to the assumptions for proving the goal with its assumptions. A counterexample is printed if the goal cannot be proved. In contrast to SmtZ3Tac, this tactic abstracts atoms to propositional variables, so that an atom like n+1==1+n can be made false to generate a counterexample.

ThenAll applies the first tactic to generate subgoals g[0..n-1] and then applies the second tactic to all subgoals g[i].

ThenL applies the given tactic to generate subgoals g[0..n-1] and then applies tacL[i] to g[i]. It fails if the number of subgoals does not match with the number of provided tactics.

TransEventualTac makes use of the transitivity of the F operator: \[ \begin{array}{c} \Gamma\vdash \mathsf{G}(\varphi\to\mathsf{F}\psi) \\ \hline \Gamma\vdash \mathsf{G}(\varphi\to\mathsf{F}\chi) \hspace{5mm} \Gamma\vdash \mathsf{G}(\chi\to\mathsf{F}\psi) \]

TransIffTac makes use of the transitivity of equivalences: \[ \begin{array}{c} \Gamma\vdash \psi\leftrightarrow\varphi \\ \hline \Gamma\vdash\psi\leftrightarrow\alpha \hspace{5mm} \Gamma\vdash\alpha\leftrightarrow\varphi \end{array} \]

TransImpTac makes use of the transitivity of implications by interpolation: \[ \begin{array}{c} \Gamma\vdash \psi\to\varphi \\ \hline \Gamma\vdash\psi\to\alpha \hspace{5mm} \Gamma\vdash\alpha\to\varphi \end{array} \]

TransWhenTac makes use of the transitivity of the W operator: \[ \begin{array}{c} \Gamma\vdash \mathsf{G}(\alpha\to[[\beta\;\mathsf{W}\;\gamma]\;\mathsf{W}\;\delta]) \\ \hline \Gamma\vdash \mathsf{G}(\alpha\to[\chi\;\mathsf{W}\;\delta]) \hspace{5mm} \Gamma\vdash \mathsf{G}(\chi\wedge\delta\to[\beta\;\mathsf{W}\;\gamma]) \]

UndischTac moves a chosen assumption to the conclusion by creating an implication: \[ \begin{array}{c} \varphi,\Gamma\vdash\psi \\ \hline \Gamma\vdash\varphi\to\psi \end{array} \]

undo the previous tactic that was applied to the current proof goal (it will fail if the current proof goal is its root goal; in that case you should use function RemoveCurrGoal).

UnrollTempOpsTac unrolls temporal logic operators such that all temporal operators will occur under Next, PastWeakNext, or PastStrongNext.

scriptMode being true will print messages when loading modules and proving theorems which is the desired output in scripting mode

verboseMode being true will print messages of the tactics which is used in the interactive mode and may be disabled in scripting mode