Automating inductionless induction using test sets
From MaRDI portal
Publication:758216
DOI10.1016/S0747-7171(08)80133-2zbMath0724.68079MaRDI QIDQ758216
Deepak Kapur, Paliath Narendran, Han-Tao Zhang
Publication date: 1991
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
completionrewritingtest setsground-reducibilityinductionless inductionproof by consistencysufficient-completeness
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
Proving ground confluence and inductive validity in constructor based equational specifications ⋮ Towards an efficient construction of test sets for deciding ground reducibility ⋮ Induction using term orders ⋮ Test sets for the universal and existential closure of regular tree languages. ⋮ Superposition for Fixed Domains ⋮ AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS ⋮ A general framework to build contextual cover set induction provers ⋮ Induction using term orderings ⋮ Deciding the Inductive Validity of ∀ ∃ * Queries ⋮ Deciding quasi-reducibility using witnessed test sets ⋮ Observational proofs by rewriting. ⋮ Deductive and inductive synthesis of equational programs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proofs by induction in equational theories with constructors
- On ground-confluence of term rewriting systems
- On sufficient-completeness and related properties of term rewriting systems
- Proof by consistency
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- The algebraic specification of abstract data types
- Automatic proofs by induction in theories without constructors
- Sufficient-completeness, ground-reducibility and their complexity
- Semantic confluence tests and completion methods
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
This page was built for publication: Automating inductionless induction using test sets
