scientific article
From MaRDI portal
Publication:2751365
zbMath0994.03007MaRDI QIDQ2751365
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
rewritinginductionautomated theorem provingripplingexplicitly inductive theorem provingsearch control problems
Related Items (29)
Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Sound generalizations in mathematical induction ⋮ Verification as a parameterized testing (experiments with the SCP4 supercompiler) ⋮ What is a proof? ⋮ Mathematical induction in Otter-lambda ⋮ Deaccumulation techniques for improving provability ⋮ The problem of \(\Pi_{2}\)-cut-introduction ⋮ Automated mutual induction proof in separation logic ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An approach to automatic deductive synthesis of functional programs ⋮ Herbrand's theorem and term induction ⋮ A Decidable Class of Nested Iterated Schemata ⋮ Perfect Discrimination Graphs: Indexing Terms with Integer Exponents ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ Shallow confluence of conditional term rewriting systems ⋮ Combining induction and saturation-based theorem proving ⋮ Schematic Cut Elimination and the Ordered Pigeonhole Principle ⋮ Appropriate lemmae discovery ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Inductive theorem proving based on tree grammars
Uses Software
This page was built for publication:
