Automatic proofs by induction in theories without constructors
From MaRDI portal
Publication:1824382
DOI10.1016/0890-5401(89)90062-XzbMath0682.68032OpenAlexW2056774266MaRDI QIDQ1824382
Jean-Pierre Jouannaud, Emmanuel Kounalis
Publication date: 1989
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0890-5401(89)90062-x
equational reasoningterm rewriting systemsinitial algebraInductionless inductioninductive co-reducibilityinductive completion algorithminductive reducibilityKnuth- Bendix completion algorithm
Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65) Thue and Post systems, etc. (03D03)
Related Items
Consistency and semantics of equational definitions over predefined algebras, Sound generalizations in mathematical induction, Ground reducibility is EXPTIME-complete, Proof by consistency, Computing ground reducibility and inductively complete positions, Inductive proofs by specification transformations, Conditional rewrite rule systems with built-in arithmetic and induction, Proofs in parameterized specifications, Proving equational and inductive theorems by completion and embedding techniques, The negation elimination from syntactic equational formula is decidable, Encompassment properties and automata with constraints, More problems in rewriting, Towards an efficient construction of test sets for deciding ground reducibility, Problems in rewriting III, Rewriting with a nondeterministic choice operator, 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, Equational problems and disunification, Applying term rewriting methods to finite groups, Abstract data type systems, Test sets for the universal and existential closure of regular tree languages., Model-theoretic aspects of unification, Pumping, cleaning and symbolic constraints solving, Specification and proof in membership equational logic, Using induction and rewriting to verify and complete parameterized specifications, Towards a foundation of completion procedures as semidecision procedures, Narrowing based procedures for equational disunification, Testing for the ground (co-)reducibility property in term-rewriting systems, AC complement problems: Satisfiability and negation elimination, Proving weak properties of rewriting, A general framework to build contextual cover set induction provers, Induction using term orderings, Mechanizable inductive proofs for a class of ∀ ∃ formulas, On the connection between narrowing and proof by consistency, Automating inductionless induction using test sets, Automatic proofs by induction in theories without constructors, Deciding quasi-reducibility using witnessed test sets, Induction = I-axiomatization + first-order consistency., Automata-driven automated induction, The equational part of proofs by structural induction, Deductive and inductive synthesis of equational programs
Cites Work
- Proofs by induction in equational theories with constructors
- REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- An overview of the Tecton proof system
- Automatic proofs by induction in theories without constructors
- Process algebra for synchronous communication
- Completion of a Set of Rules Modulo a Set of Equations
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
