On notions of inductive validity for first-order equational clauses
From MaRDI portal
Publication:5210769
Recommendations
- Proving ground confluence and inductive validity in constructor based equational specifications
- Automatic proofs by induction in theories without constructors
- scientific article; zbMATH DE number 1302503
- Induction = I-axiomatization + first-order consistency.
- Inductive proofs by specification transformations
Cites work
- A constructor-based approach for positive/negative-conditional equational specifications
- Automated Mathematical Induction
- scientific article; zbMATH DE number 4090848 (Why is no real title available?)
- scientific article; zbMATH DE number 4090852 (Why is no real title available?)
- scientific article; zbMATH DE number 4089521 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 4776 (Why is no real title available?)
- Inductive theorem proving by consistency for first-order clauses
- Order-sorted unification
- Proof by consistency
- Proof by consistency in conditional equational theories
- Semantics for positive/negative conditional rewrite systems
Cited in
(7)- Induction using term orders
- Shallow confluence of conditional term rewriting systems
- Deciding the Inductive Validity of ∀ ∃ * Queries
- Proving ground confluence and inductive validity in constructor based equational specifications
- Induction using term orderings
- A general framework to build contextual cover set induction provers
- A unified view of induction reasoning for first-order logic
This page was built for publication: On notions of inductive validity for first-order equational clauses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5210769)
