Lines Matching defs:logic
46 definitional\/} approach to using higher order logic. That is, the syntax of
47 the logic is extended with new notation not simply by postulating axioms to
49 of the logic that already have the required semantics. The advantage of this
51 rules of definition in the {\small HOL} logic---namely, constant definition,
63 {\small HOL} logic. But certain recursive type definitions and function
73 set of rules. \mbox{Sections~\ref{ind-defs}} and~\ref{in-logic} give a general
195 \section{Inductive definitions in logic}\label{in-logic}
201 straightforward to express this concept in logic.
223 the form discussed above can be expressed in logic in a similar way.
235 ${\sf Rtc}\;R$ can be defined in the {\small HOL} logic by the constant
259 defined formally in the {\small HOL} logic by a constant definition of the kind
437 The constant {\sf Rtc} defined in section~\ref{in-logic} is not itself an
862 relation for combinatory logic and a proof that it has the Church-Rosser
864 for minimal intuitionistic logic; the definition of a type system for
865 combinatory logic and a proof of the Curry-Howard isomorphism for typed
866 combinatory logic and minimal intuitionistic logic; and definitions of the