Automating inductionless induction using test sets

DOI10.1016/S0747-7171(08)80133-2MaRDI QIDQ758216zbMATH OpenFDO

Authors Deepak Kapur, Paliath Narendran, Hantao Zhang

Publication date 1991

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

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)

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

Cites work

• scientific article; zbMATH DE number 3649988 (Why is no real title available?)
• scientific article; zbMATH DE number 3928346 (Why is no real title available?)
• scientific article; zbMATH DE number 3943001 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 4074541 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3776841 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Automatic proofs by induction in theories without constructors
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• On ground-confluence of term rewriting systems
• On sufficient-completeness and related properties of term rewriting systems
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Proof by consistency
• Proofs by induction in equational theories with constructors
• Semantic confluence tests and completion methods
• Sufficient-completeness, ground-reducibility and their complexity
• The algebraic specification of abstract data types

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
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• Towards an efficient construction of test sets for deciding ground reducibility
• 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

Describes a project that uses

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)