Handbook of Automated Reasoning, Volume 1Alan J.A. Robinson, Andrei Voronkov Handbook of Automated Reasoning |
Other editions - View all
Handbook of Automated Reasoning, Volume 2 John Alan Robinson,Andreĭ Voronkov No preview available - 2001 |
Common terms and phrases
algebraic algorithm applied approach assume atom Automated Reasoning axioms basic branch calculus called chapter clauses closed combination complete Computer Computer Science conclusion connection consider consists constants constraint construction contains corresponding decidable defined definition denote derivation E-unification elimination equality equations equivalent example exists expressions extension Figure finite first-order formula function geometry given ground induction inference instance introduced intuitionistic logic inverse lemma linear literals logic method minimal multiset normal form Note obtained occur ordering pair paramodulation path polynomial positive possible premises problem procedure programming proof quantifier recursive reduction redundant refutation relation replaced represented resolution respect restrictions rewrite rigid rule satisfiable saturated selection sequent simplification Skolem solution solving standard step structure subformula substitution symbols tableau techniques termination theorem proving theory transformation true unification unifier University variables Voronkov