A general framework to build contextual cover set induction provers (Q5950934): Difference between revisions

@@ Property / cites work @@
+Mechanizing structural induction. II: Strategies
@@ Property / cites work: Mechanizing structural induction. II: Strategies / rank @@
+Normal rank
@@ Property / cites work @@
+Q4336265
@@ Property / cites work: Q4336265 / rank @@
+Normal rank
@@ Property / cites work @@
+Buchberger's algorithm: A constraint-based completion procedure
+Normal rank
@@ Property / cites work @@
+Q4693774
@@ Property / cites work: Q4693774 / rank @@
+Normal rank
@@ Property / cites work @@
+Behavioural approaches to algebraic specifications. A comparative study
+Normal rank
@@ Property / cites work @@
+Proof by consistency in conditional equational theories
+Normal rank
@@ Property / cites work @@
+Q5762080
@@ Property / cites work: Q5762080 / rank @@
+Normal rank
@@ Property / cites work @@
+Using induction and rewriting to verify and complete parameterized specifications
+Normal rank
@@ Property / cites work @@
+Automated theorem proving by test set induction
@@ Property / cites work: Automated theorem proving by test set induction / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Mathematical Induction
@@ Property / cites work: Automated Mathematical Induction / rank @@
+Normal rank
@@ Property / cites work @@
+Implicit induction in conditional theories
@@ Property / cites work: Implicit induction in conditional theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q3490989
@@ Property / cites work: Q3490989 / rank @@
+Normal rank
@@ Property / cites work @@
+Conditional rewriting in focus
@@ Property / cites work: Conditional rewriting in focus / rank @@
+Normal rank
@@ Property / cites work @@
+Induction using term orders
@@ Property / cites work: Induction using term orders / rank @@
+Normal rank
@@ Property / cites work @@
+Orderings for term-rewriting systems
@@ Property / cites work: Orderings for term-rewriting systems / rank @@
+Normal rank
@@ Property / cites work @@
+Proving termination with multiset orderings
@@ Property / cites work: Proving termination with multiset orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Q3221381
@@ Property / cites work: Q3221381 / rank @@
+Normal rank
@@ Property / cites work @@
+A strong restriction of the inductive completion procedure
+Normal rank
@@ Property / cites work @@
+Q3943975
@@ Property / cites work: Q3943975 / rank @@
+Normal rank
@@ Property / cites work @@
+Proofs by induction in equational theories with constructors
+Normal rank
@@ Property / cites work @@
+Automatic proofs by induction in theories without constructors
+Normal rank
@@ Property / cites work @@
+Automating inductionless induction using test sets
+Normal rank
@@ Property / cites work @@
+Proofs in parameterized specifications
@@ Property / cites work: Proofs in parameterized specifications / rank @@
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4712663
@@ Property / cites work: Q4712663 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3427354
@@ Property / cites work: Q3427354 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4139711
@@ Property / cites work: Q4139711 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3034806
@@ Property / cites work: Q3034806 / rank @@
+Normal rank
@@ Property / cites work @@
+Deduction and Declarative Programming
@@ Property / cites work: Deduction and Declarative Programming / rank @@
+Normal rank
@@ Property / cites work @@
+On notions of inductive validity for first-order equational clauses
+Normal rank
@@ Property / cites work @@
+Q3805961
@@ Property / cites work: Q3805961 / rank @@
+Normal rank