scientific article; zbMATH DE number 4053061

MaRDI QIDQ3789100zbMATH OpenFDO

Authors Deepak Kapur, Hantao Zhang

Publication date 1988

zbMATH Keywords

theorem provingconditional rewritingSchubert's steamrollerfirst-order predicate calculus with equalitysuperposition on maximal literals in clauses

Mathematics Subject Classification ID

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

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

(25)

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

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)