Checking Sufficient Completeness by Inductive Theorem Proving

DOI10.1007/978-3-031-12441-9_9zbMath1514.68038MaRDI QIDQ6487296

José Meseguer

Publication date: 7 December 2022

Mathematics Subject Classification ID

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

Related Items (1)

On Ground Convergence and Completeness of Conditional Equational Program Hierarchies

Cites Work

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

This page was built for publication: Checking Sufficient Completeness by Inductive Theorem Proving