scientific article; zbMATH DE number 4053061

MaRDI QIDQ3789100zbMATH OpenFDO

Authors Deepak Kapur, Hantao Zhang

Publication date 1988

zbMATH Keywords

conditional rewritingfirst-order predicate calculus with equalitySchubert's steamrollersuperposition on maximal literals in clausestheorem proving

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Partial orders, general (06A06) Symbolic computation and algebraic computation (68W30)

Recommendations

• Conditional term rewriting and first-order theorem proving
• scientific article; zbMATH DE number 4090849
• Well-behaved inference rules for first-order theorem proving
• scientific article; zbMATH DE number 1300967
• Inductive theorem proving by consistency for first-order clauses
• scientific article; zbMATH DE number 1070624
• scientific article; zbMATH DE number 46359
• Rewrite method for theorem proving in first order theory with equality
• First-order theorem proving: foreword
• Certifying proofs in the first-order theory of rewriting

Cited in

(26)

• Conditional narrowing modulo a set of equations
• Deductive and inductive synthesis of equational programs
• Proving Ramsey's theory by the cover set induction: A case and comparision study.
• Conditional congruence closure over uninterpreted and interpreted symbols
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• Linear and unit-resulting refutations for Horn theories
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• scientific article; zbMATH DE number 4203770 (Why is no real title available?)
• scientific article; zbMATH DE number 4090849 (Why is no real title available?)
• scientific article; zbMATH DE number 1507183 (Why is no real title available?)
• Harald Ganzinger's legacy: contributions to logics and programming
• From search to computation: redundancy criteria and simplification at work
• Proof normalization for resolution and paramodulation
• Reduction techniques for first-order reasoning
• Conditional term rewriting and first-order theorem proving
• Proving group isomorphism theorems
• Implementing contextual rewriting
• Conditional rewriting in focus
• A maximal-literal unit strategy for horn clauses
• Completion procedures as semidecision procedures
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• On restrictions of ordered paramodulation with simplification
• Dissolver: A dissolution-based theorem prover
• Towards a foundation of completion procedures as semidecision procedures
• Using forcing to prove completeness of resolution and paramodulation

Describes a project that uses

Uses Software

• RRL

This page was built for publication:

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