Lines Matching defs:sequent
2 \index{sequent calculus|(}
5 sequent calculus (see Gallier~\cite{gallier86} or Takeuti~\cite{takeuti87}).
80 sequent $\Gamma\turn \Delta$
194 In a sequent, anything not prefixed by \verb|$| is taken as a formula.
278 required; all the formulae{} in the sequent will be simplified. The left-hand
291 provided for the sequent calculus. Two commands are available for adding new
292 sequent calculus rules, safe or unsafe, to the default ``theorem pack'':
299 and~\ref{sec:sequent-provers} give full details.
309 the sequent \(P\conj Q\turn Q\conj P\).
325 formula is given as a string, and replaces some other formula in the sequent.
352 returns the list of all formulae in the sequent~$t$, removing sequence
372 Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.
405 Because LK is a sequent calculus, the formula~$P(\Var{x})$ does not become an
407 be instantiated to a basic sequent: the bound variable~$x$ is not unifiable
499 and create a basic sequent.
540 This technique lets Isabelle formalize sequent calculus rules,
548 LK exploits this representation of lists. As an alternative, the sequent
558 \section{*Packaging sequent rules}\label{sec:thm-pack}
560 The sequent calculi come with simple proof procedures. These are incomplete
565 proof. For instance, all the standard rules of the classical sequent calculus
626 \section{*Proof procedures}\label{sec:sequent-provers}
711 \index{sequent calculus|)}