Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
From MaRDI portal
Cites work
- A certified algorithm for AC-unification
- A fully syntactic AC-RPO.
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Checking Sufficient Completeness by Inductive Theorem Proving
- Conditional rewriting logic as a unified model of concurrency
- Coverset induction with partiality and subsorts: a powerlist case study
- Equational rules for rewriting logic
- Folding variant narrowing and optimal variant termination
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 3817070 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 3684925 (Why is no real title available?)
- scientific article; zbMATH DE number 3703962 (Why is no real title available?)
- scientific article; zbMATH DE number 50648 (Why is no real title available?)
- scientific article; zbMATH DE number 517385 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 794241 (Why is no real title available?)
- Implicit induction in conditional theories
- Induction = I-axiomatization + first-order consistency.
- Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Metalevel algorithms for variant satisfiability
- Methods for proving termination of rewriting-based programming languages by transformation
- MTT: The Maude Termination Tool (System Description)
- Normal form transformations
- Normal forms and normal theories in conditional rewriting
- On Automation of OTS/CafeOBJ Method
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Operational termination of conditional term rewriting systems
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Order-Sorted Rewriting and Congruence Closure
- Ordered rewriting and confluence
- Paramodulation-based theorem proving
- Proof by consistency
- Proofs by induction in equational theories with constructors
- Proving and rewriting
- Proving Safety Properties of Rewrite Theories
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Semantic foundations for generalized rewrite theories
- Termination Modulo Combinations of Equational Theories
- Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
- Theorem proving modulo associativity
- Twenty years of rewriting logic
- Variants and satisfiability in the infinitary unification wonderland
- Verification of the IBOS Browser Security Properties in Reachability Logic
Cited in
(4)- DM-check: verifying invariants of concurrent systems by deductive model checking
- Equational reasoning modulo commutativity in languages with binders
- Preface to rewriting logic and its applications (revised selected papers from WRLA 2020)
- NuITP: accelerating the inductive verification of equational programs through symbolic simplification
This page was built for publication: Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7009392)
