Lines Matching refs:first
3 \index{first-order logic|(}
6 nk}. Intuitionistic first-order logic is defined first, as theory
15 first-order terms is called \cldx{term} and is a subclass of \isa{logic}.
249 for first-order logic because they discard universally quantified
299 depth-first search, to solve subgoal~$i$.
302 best-first search (guided by the size of the proof state) to solve subgoal~$i$.
466 Q)\disj (Q\imp P)$. The first step is apply the
538 above. Its key step is its first rule, \tdx{exCI}, a classical
612 Classical first-order logic can be extended with the propositional
736 In the first two subgoals, all assumptions have been reduced to atoms. Now
757 Where do we stand? The first subgoal holds by assumption; the second and
759 reasoner, but first let us extend the default claset with the derived rules
789 We are left with a subgoal in pure first-order logic, and it falls to
798 times faster than proofs using just the rules of first-order logic.
827 first-order logic:
855 \index{first-order logic|)}