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
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, 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
