Checking Sufficient Completeness by Inductive Theorem Proving
From MaRDI portal
Publication:6487296
Recommendations
- scientific article; zbMATH DE number 1761886
- Proving equational and inductive theorems by completion and embedding techniques
- Inductive completeness of logics of programs
- scientific article; zbMATH DE number 1670785
- Combining induction and saturation-based theorem proving
- Proving completeness for nested sequent calculi
- Methods for proving completeness via logical reductions
- Completeness in Proof-Theoretic Semantics
- Verifying programs in the calculus of inductive constructions
Cites work
- scientific article; zbMATH DE number 4049024 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- A proof method for local sufficient completeness of term rewriting systems
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Automata-driven automated induction
- Automatic proofs by induction in theories without constructors
- CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
- Conditional rewriting logic as a unified model of concurrency
- Equational formulas and pattern operations in initial order-sorted algebras
- Explicit representation of terms defined by counter examples
- Folding variant narrowing and optimal variant termination
- Ground confluence of order-sorted conditional specifications modulo axioms
- Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
- Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
- Normal forms and normal theories in conditional rewriting
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- On the Completeness of Context-Sensitive Order-Sorted Specifications
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Simultaneous checking of completeness and ground confluence for algebraic specifications
- Specification and proof in membership equational logic
- Sufficient-completeness, ground-reducibility and their complexity
- Term Rewriting and Applications
- Term Rewriting and Applications
- Termination Modulo Combinations of Equational Theories
- The algebraic specification of abstract data types
- Variant-Based Satisfiability in Initial Algebras
Cited in
(5)- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- Online Enumeration of All Minimal Inductive Validity Cores
- scientific article; zbMATH DE number 4011938 (Why is no real title available?)
- Using an induction prover for verifying arithmetic circuits
- Building correct-by-construction systems with formal patterns
This page was built for publication: Checking Sufficient Completeness by Inductive Theorem Proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6487296)
