Proof by consistency

DOI10.1016/0004-3702(87)90017-8zbMath0631.68073OpenAlexW2001026998MaRDI QIDQ1094888

Deepak Kapur, David R. Musser

Publication date: 1987

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(87)90017-8

zbMATH Keywords

inductionless inductionproof by consistencyfirst-order equationsconsistency of proof systems

Mathematics Subject Classification ID

Relative consistency and interpretations (03F25)

Related Items (30)

A constructor-based approach for positive/negative-conditional equational specifications ⋮ Completion procedures as semidecision procedures ⋮ Proving ground confluence and inductive validity in constructor based equational specifications ⋮ Implicit induction in conditional theories ⋮ Computing ground reducibility and inductively complete positions ⋮ Inductive proofs by specification transformations ⋮ An overview of LP, the Larch Prover ⋮ Proving equational and inductive theorems by completion and embedding techniques ⋮ An algebraic characterization of inductive soundness in proof by consistency ⋮ Proving Ramsey's theory by the cover set induction: A case and comparision study. ⋮ Sufficient-completeness, ground-reducibility and their complexity ⋮ Only prime superpositions need be considered in the Knuth-Bendix completion procedure ⋮ Induction using term orders ⋮ Model building with ordered resolution: Extracting models from saturated clause sets ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Termination of algorithms over non-freely generated data types ⋮ Abstract canonical presentations ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness ⋮ Proving semantic properties as first-order satisfiability ⋮ Induction using term orderings ⋮ On notions of inductive validity for first-order equational clauses ⋮ Unification modulo lists with reverse relation with certain word equations ⋮ Automating inductionless induction using test sets ⋮ Induction = I-axiomatization + first-order consistency. ⋮ Which data types have \(\omega\)-complete initial algebra specifications? ⋮ Finite reasons for safety ⋮ Deductive and inductive synthesis of equational programs

Cites Work

• Final algebra semantics and data type extensions
• The algebraic specification of abstract data types
• Automatic proofs by induction in theories without constructors
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Final Data Types and Their Specification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof by consistency