Lines Matching defs:logic
9 special screen font. The meta-logic and main object-logics already
13 meta-logic and provides certain fundamental data structures: types,
23 and demonstrates forward proof. The examples are set in first-order logic.
24 The command to start Isabelle running first-order logic is
28 Note that just typing \texttt{isabelle} usually brings up higher-order logic
42 the syntax of the meta-logic.) Such symbols may be run together; thus if
74 Classes are denoted by identifiers; the built-in class \cldx{logic}
116 The theorems and rules of an object-logic are represented by theorems in
117 the meta-logic, which are expressed using meta-formulae. Since the
118 meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
172 To illustrate the notation, consider two axioms for first-order logic:
180 cluttering logic definitions with question marks, Isabelle converts any
203 theorems and inference rules of object-logics. Isabelle's meta-logic is
237 first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
466 \subsection{A trivial example in propositional logic}
470 first-order logic. Let us try the example from \S\ref{prop-proof},
700 first-order logic. I have elsewhere proved the faithfulness of Isabelle's
701 encoding of first-order logic~\cite{paulson-found}; there could, of course, be
898 reasoner can be set up for any classical natural deduction logic;