scientific article
From MaRDI portal
Publication:3805961
zbMath0657.68103MaRDI QIDQ3805961
Deepak Kapur, Han-Tao Zhang, Mukkai S. Krishnamoorthy
Publication date: 1988
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35)
Related Items
Sound generalizations in mathematical induction ⋮ An overview of the Tecton proof system ⋮ Implicit induction in conditional theories ⋮ Computing ground reducibility and inductively complete positions ⋮ A recursion planning analysis of inductive completion ⋮ Proving Ramsey's theory by the cover set induction: A case and comparision study. ⋮ Induction using term orders ⋮ New uses of linear arithmetic in automated theorem proving by induction ⋮ Reasoning with conditional axioms ⋮ Automated reasoning about parallel algorithms using powerlists ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Using induction and rewriting to verify and complete parameterized specifications ⋮ Termination of algorithms over non-freely generated data types ⋮ Lemma discovery in automating induction ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ A general framework to build contextual cover set induction provers ⋮ Mechanizable inductive proofs for a class of ∀ ∃ formulas ⋮ Automating inductionless induction using test sets ⋮ Appropriate lemmae discovery ⋮ Automata-driven automated induction ⋮ Proving termination of (conditional) rewrite systems. A semantic approach
