scientific article; zbMATH DE number 4053061
From MaRDI portal
Publication:3789100
zbMATH Open0645.68096MaRDI QIDQ3789100FDOQ3789100
Authors: Deepak Kapur, Hantao Zhang 
Publication date: 1988
Title of this publication is not available (Why is that?)
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
theorem provingconditional rewritingSchubert's steamrollerfirst-order predicate calculus with equalitysuperposition on maximal literals in clauses
Partial orders, general (06A06) Symbolic computation and algebraic computation (68W30) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)
Cited In (25)
- Deductive and inductive synthesis of equational programs
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- On restrictions of ordered paramodulation with simplification
- Conditional congruence closure over uninterpreted and interpreted symbols
- Proving group isomorphism theorems
- Implementing contextual rewriting
- Conditional narrowing modulo a set of equations
- A maximal-literal unit strategy for horn clauses
- Title not available (Why is that?)
- Harald Ganzinger's legacy: contributions to logics and programming
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Conditional term rewriting and first-order theorem proving
- Towards a foundation of completion procedures as semidecision procedures
- Proof normalization for resolution and paramodulation
- Reduction techniques for first-order reasoning
- Title not available (Why is that?)
- 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
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Proving Ramsey's theory by the cover set induction: A case and comparision study.
- Completion procedures as semidecision procedures
- Conditional rewriting in focus
- Linear and unit-resulting refutations for Horn theories
- Using forcing to prove completeness of resolution and paramodulation
Uses Software
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)
