Implicit induction in conditional theories
From MaRDI portal
Publication:1891255
DOI10.1007/BF00881856zbMath0819.68114MaRDI QIDQ1891255
Michaël Rusinowitch, Adel Bouhoula
Publication date: 30 May 1995
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items
Productive use of failure in inductive proof, Deaccumulation techniques for improving provability, Incorporating decision procedures in implicit induction., Sufficient completeness verification for conditional and constrained TRS, Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities, Automated Induction with Constrained Tree Automata, Specification and proof in membership equational logic, Using induction and rewriting to verify and complete parameterized specifications, AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS, Unraveling a Card Trick, Perfect Discrimination Graphs: Indexing Terms with Integer Exponents, A general framework to build contextual cover set induction provers, On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs, Generalized rewrite theories, coherence completion, and symbolic methods, A divergence critic, Combining induction and saturation-based theorem proving, Using a generalisation critic to find bisimulations for coinductive proofs, Inductive proof search modulo, Induction = I-axiomatization + first-order consistency., Automata-driven automated induction, Narrowing and Rewriting Logic: from Foundations to Applications, Observational proofs by rewriting.
Uses Software
Cites Work
