Pages that link to "Item:Q789177"

The following pages link to Proofs by induction in equational theories with constructors (Q789177):

Displaying 50 items.

• Sufficient completeness verification for conditional and constrained TRS (Q420848) (← links)
• Proving weak properties of rewriting (Q554217) (← links)
• Building exact computation sequences (Q579925) (← links)
• Order-sorted unification (Q582269) (← links)
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness (Q582891) (← links)
• Using induction and rewriting to verify and complete parameterized specifications (Q672051) (← links)
• Towards a foundation of completion procedures as semidecision procedures (Q673134) (← links)
• Testing for the ground (co-)reducibility property in term-rewriting systems (Q685352) (← links)
• Automating inductionless induction using test sets (Q758216) (← links)
• Mechanizing and improving dependency pairs (Q877836) (← links)
• Equational completion in order-sorted algebras (Q912606) (← links)
• Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories (Q1059404) (← links)
• Conditional rewrite rules (Q1065790) (← links)
• On sufficient-completeness and related properties of term rewriting systems (Q1077161) (← links)
• Partial evaluation and \(\omega\)-completeness of algebraic specifications (Q1084849) (← links)
• On solving the equality problem in theories defined by Horn clauses (Q1085152) (← links)
• Unification in combinations of collapse-free regular theories (Q1099652) (← links)
• Simplifying conditional term rewriting systems: Unification, termination and confluence (Q1100891) (← links)
• History and basic features of the critical-pair/completion procedure (Q1103414) (← links)
• Critical pair criteria for completion (Q1106659) (← links)
• Narrowing based procedures for equational disunification (Q1197097) (← links)
• Schematization of infinite sets of rewrite rules generated by divergent completion processes (Q1262755) (← links)
• The equational part of proofs by structural induction (Q1317862) (← links)
• Deductive and inductive synthesis of equational programs (Q1322836) (← links)
• A recursion planning analysis of inductive completion (Q1353935) (← links)
• Abstract data type systems (Q1391729) (← links)
• Test sets for the universal and existential closure of regular tree languages. (Q1400712) (← links)
• Partial completion of equational theories (Q1592635) (← links)
• Automatic proofs by induction in theories without constructors (Q1824382) (← links)
• Induction = I-axiomatization + first-order consistency. (Q1854350) (← links)
• Sound generalizations in mathematical induction (Q1882908) (← links)
• Implicit induction in conditional theories (Q1891255) (← links)
• Induction using term orders (Q1915132) (← links)
• Reasoning with conditional axioms (Q1924731) (← links)
• Specification and proof in membership equational logic (Q1978640) (← links)
• Sufficient-completeness, ground-reducibility and their complexity (Q2641108) (← links)
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS (Q3021959) (← links)
• (Q3327710) (← links)
• (Q3667939) (← links)
• (Q3675498) (← links)
• Comparing data type specifications via their normal forms (Q3949956) (← links)
• Size-based termination of higher-order rewriting (Q4577817) (← links)
• Proving ground confluence and inductive validity in constructor based equational specifications (Q5044723) (← links)
• Computing ground reducibility and inductively complete positions (Q5055712) (← links)
• Inductive proofs by specification transformations (Q5055713) (← links)
• An overview of LP, the Larch Prover (Q5055717) (← links)
• Conditional rewrite rule systems with built-in arithmetic and induction (Q5055742) (← links)
• Applying term rewriting methods to finite groups (Q5096205) (← links)
• Induction using term orderings (Q5210765) (← links)
• Mechanizable inductive proofs for a class of ∀ ∃ formulas (Q5210766) (← links)