scientific article
From MaRDI portal
Publication:3789100
zbMath0645.68096MaRDI QIDQ3789100
Publication date: 1988
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
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)
Related Items (21)
Reduction techniques for first-order reasoning ⋮ Proving group isomorphism theorems ⋮ Implementing contextual rewriting ⋮ Conditional rewriting in focus ⋮ A maximal-literal unit strategy for horn clauses ⋮ Completion procedures as semidecision procedures ⋮ Proof normalization for resolution and paramodulation ⋮ Proving Ramsey's theory by the cover set induction: A case and comparision study. ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ On restrictions of ordered paramodulation with simplification ⋮ Dissolver: A dissolution-based theorem prover ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Conditional narrowing modulo a set of equations ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II ⋮ Deductive and inductive synthesis of equational programs
Uses Software
This page was built for publication:
