On notions of inductive validity for first-order equational clauses

DOI10.1007/3-540-58156-1_12zbMath1437.03050OpenAlexW1571394616MaRDI QIDQ5210769

Claus-Peter Wirth, Bernhard Gramlich

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_12

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Induction using term orders, A general framework to build contextual cover set induction provers, Shallow confluence of conditional term rewriting systems, Induction using term orderings

Cites Work

• Order-sorted unification
• Proof by consistency
• Automated Mathematical Induction
• A constructor-based approach for positive/negative-conditional equational specifications
• Semantics for positive/negative conditional rewrite systems
• Inductive theorem proving by consistency for first-order clauses
• Proof by consistency in conditional equational theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item