Checking Sufficient Completeness by Inductive Theorem Proving

DOI10.1007/978-3-031-12441-9_9zbMATH Open1514.68038MaRDI QIDQ6487296FDOQ6487296

Publication date: 7 December 2022

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

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)

Cites Work

All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
Title not available (Why is that?)
CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
Conditional rewriting logic as a unified model of concurrency
Title not available (Why is that?)
Normal forms and normal theories in conditional rewriting
The algebraic specification of abstract data types
Automata-driven automated induction
Specification and proof in membership equational logic
Sufficient-completeness, ground-reducibility and their complexity
Title not available (Why is that?)
Term Rewriting and Applications
On the Completeness of Context-Sensitive Order-Sorted Specifications
Simultaneous checking of completeness and ground confluence for algebraic specifications
Term Rewriting and Applications
Automatic proofs by induction in theories without constructors
Explicit representation of terms defined by counter examples
On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
Folding variant narrowing and optimal variant termination
Termination Modulo Combinations of Equational Theories
Variant-Based Satisfiability in Initial Algebras
Equational formulas and pattern operations in initial order-sorted algebras
On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
A proof method for local sufficient completeness of term rewriting systems
Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
Ground confluence of order-sorted conditional specifications modulo axioms
Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications

Cited In (5)

Using an induction prover for verifying arithmetic circuits
Building correct-by-construction systems with formal patterns
Online Enumeration of All Minimal Inductive Validity Cores
Title not available (Why is that?)
On Ground Convergence and Completeness of Conditional Equational Program Hierarchies

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)