Automating inductionless induction using test sets

DOI10.1016/S0747-7171(08)80133-2zbMATH Open0724.68079MaRDI QIDQ758216FDOQ758216

Authors: Deepak Kapur, Paliath Narendran, Hantao Zhang 

Publication date: 1991

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

Recommendations

• scientific article; zbMATH DE number 4047063
• Automatic proofs by induction in theories without constructors
• Automated theorem proving by test set induction
• scientific article; zbMATH DE number 4776
• scientific article; zbMATH DE number 3891336

zbMATH Keywords

rewritingcompletiontest setsground-reducibilityinductionless inductionproof by consistencysufficient-completeness

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Equational classes, universal algebra in model theory (03C05)

Cites Work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Title not available (Why is that?)
• Title not available (Why is that?)
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Title not available (Why is that?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• On sufficient-completeness and related properties of term rewriting systems
• The algebraic specification of abstract data types
• Sufficient-completeness, ground-reducibility and their complexity
• Proofs by induction in equational theories with constructors
• On ground-confluence of term rewriting systems
• Proof by consistency
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic proofs by induction in theories without constructors
• Semantic confluence tests and completion methods
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (18)

• Deductive and inductive synthesis of equational programs
• Superposition for Fixed Domains
• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
• An induction machine and power electronic test system on a field-programmable gate array
• Induction using term orders
• Proving ground confluence and inductive validity in constructor based equational specifications
• Deciding quasi-reducibility using witnessed test sets
• Automatic proofs by induction in theories without constructors
• Deciding inductive validity of equations.
• Observational proofs by rewriting.
• Deciding the Inductive Validity of ∀ ∃ * Queries
• Self-Testing without the Generator Bottleneck
• Towards an efficient construction of test sets for deciding ground reducibility
• Title not available (Why is that?)
• Induction using term orderings
• Inductionless induction
• Test sets for the universal and existential closure of regular tree languages.
• A general framework to build contextual cover set induction provers

Uses Software

• RRL

This page was built for publication: Automating inductionless induction using test sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q758216)