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
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, 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
