Proofs by induction in equational theories with constructors

DOI10.1016/0022-0000(82)90006-XzbMath0532.68041OpenAlexW2021173362MaRDI QIDQ789177

Publication date: 1982

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(82)90006-x

zbMATH Keywords

equational logic data structures algebraic-summation identities extension of the Knuth-Bendix completion algorithm initial algebra of an equational variety program proving

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Equational logic, Mal'tsev conditions (08B05) General topics in the theory of software (68N01) Software, source code, etc. for problems pertaining to general algebraic systems (08-04)

Related Items

On sufficient-completeness and related properties of term rewriting systems, Inductive theorem proving by consistency for first-order clauses, Confluence of terminating membership conditional TRS, Normalization by leftmost innermost rewriting, A proof system for conditional algebraic specifications, Completion procedures as semidecision procedures, On sufficient completeness of conditional specifications, Design strategies for rewrite rules, Verifying Procedural Programs via Constrained Rewriting Induction, Partial evaluation and \(\omega\)-completeness of algebraic specifications, On solving the equality problem in theories defined by Horn clauses, Sound generalizations in mathematical induction, Proving ground confluence and inductive validity in constructor based equational specifications, Implicit induction in conditional theories, Computing ground reducibility and inductively complete positions, Inductive proofs by specification transformations, An overview of LP, the Larch Prover, Conditional rewrite rule systems with built-in arithmetic and induction, Unification in combinations of collapse-free regular theories, A recursion planning analysis of inductive completion, Simplifying conditional term rewriting systems: Unification, termination and confluence, History and basic features of the critical-pair/completion procedure, Sufficient-completeness, ground-reducibility and their complexity, Critical pair criteria for completion, Unnamed Item, Induction using term orders, Mechanizing and improving dependency pairs, Size-based termination of higher-order rewriting, Reasoning with conditional axioms, Applying term rewriting methods to finite groups, Abstract data type systems, Test sets for the universal and existential closure of regular tree languages., Sufficient completeness verification for conditional and constrained TRS, Equational completion in order-sorted algebras, Specification and proof in membership equational logic, Unnamed Item, Using induction and rewriting to verify and complete parameterized specifications, Towards a foundation of completion procedures as semidecision procedures, Unnamed Item, Narrowing based procedures for equational disunification, Testing for the ground (co-)reducibility property in term-rewriting systems, AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS, Proving weak properties of rewriting, A general framework to build contextual cover set induction provers, Building exact computation sequences, Order-sorted unification, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, Induction using term orderings, Mechanizable inductive proofs for a class of ∀ ∃ formulas, On the connection between narrowing and proof by consistency, Schematization of infinite sets of rewrite rules generated by divergent completion processes, Automating inductionless induction using test sets, Automatic proofs by induction in theories without constructors, Partial completion of equational theories, Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories, Induction = I-axiomatization + first-order consistency., Conditional rewrite rules, Comparing data type specifications via their normal forms, The equational part of proofs by structural induction, Deductive and inductive synthesis of equational programs

Cites Work