Checking Sufficient Completeness by Inductive Theorem Proving

DOI10.1007/978-3-031-12441-9_9MaRDI QIDQ6487296zbMATH OpenFDO

Authors José Meseguer

Publication date 7 December 2022

Full work available at URL https://doi.org/10.1007/978-3-031-12441-9_9

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

• 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
• 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?)
• 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

(7)

• Using an induction prover for verifying arithmetic circuits
• scientific article; zbMATH DE number 4011938 (Why is no real title available?)
• Online Enumeration of All Minimal Inductive Validity Cores
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Building correct-by-construction systems with formal patterns
• A nominal approach to equational problems in languages with binders
• Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification

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)