A general framework to build contextual cover set induction provers

DOI10.1006/jsco.2000.0469zbMath0981.68147OpenAlexW2057086674MaRDI QIDQ5950934

Sorin Stratulat

Publication date: 2 January 2002

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.2000.0469

zbMATH Keywords

contextual cover set

Mathematics Subject Classification ID

Related Items (10)

\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} ⋮ Unnamed Item ⋮ Incorporating decision procedures in implicit induction. ⋮ Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities ⋮ Automated Induction with Constrained Tree Automata ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Correctness of Context-Moving Transformations for Term Rewriting Systems ⋮ Combining induction and saturation-based theorem proving ⋮ Automated Certification of Implicit Induction Proofs ⋮ An Undo Framework for P2P Collaborative Editing

Uses Software

• PVS
• SPIKE
• STeP
• EXPANDER
• UNICOM
• RRL

Cites Work

• Orderings for term-rewriting systems
• Using induction and rewriting to verify and complete parameterized specifications
• Automating inductionless induction using test sets
• Proofs by induction in equational theories with constructors
• Mechanizing structural induction. II: Strategies
• Behavioural approaches to algebraic specifications. A comparative study
• Automated theorem proving by test set induction
• A strong restriction of the inductive completion procedure
• Automatic proofs by induction in theories without constructors
• Implicit induction in conditional theories
• Induction using term orders
• Proving termination with multiset orderings
• Deduction and Declarative Programming
• Automated Mathematical Induction
• Proofs in parameterized specifications
• Buchberger's algorithm: A constraint-based completion procedure
• On notions of inductive validity for first-order equational clauses
• Conditional rewriting in focus
• Proof by consistency in conditional equational theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A general framework to build contextual cover set induction provers