Reduction techniques for first-order reasoning

DOI10.1007/3-540-56393-8_18MaRDI QIDQ5881189zbMATH OpenOpenAlexFDO

Authors Francois Bronsard, Uday S. Reddy

Publication date 9 March 2023

Published in Conditional Term Rewriting Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-56393-8_18

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Clausal rewriting
• scientific article; zbMATH DE number 3871320
• Equational methods in first order predicate calculus
• A completion procedure for conditional equations
• Completion of first-order clauses with equality by strict superposition

Cites work

• A completion procedure for conditional equations
• Clausal rewriting
• Completion of first-order clauses with equality by strict superposition
• Conditional rewriting in focus
• scientific article; zbMATH DE number 4049135 (Why is no real title available?)
• scientific article; zbMATH DE number 4053061 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• Proof normalization for resolution and paramodulation

Cited in

(6)

• Deductive and inductive synthesis of equational programs
• Induction using term orders
• Reductional programming of functions represented by recurrent relations of the first order
• Problems in rewriting III
• Induction using term orderings
• Clausal rewriting

This page was built for publication: Reduction techniques for first-order reasoning

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