scientific article; zbMATH DE number 1303343
From MaRDI portal
Publication:4249896
zbMATH Open0924.03017MaRDI QIDQ4249896FDOQ4249896
Authors: Leo Bachmair, Harald Ganzinger
Publication date: 7 November 1999
Title of this publication is not available (Why is that?)
Recommendations
- Completion of first-order clauses with equality by strict superposition
- On restrictions of ordered paramodulation with simplification
- scientific article; zbMATH DE number 1348470
- Superposition with equivalence reasoning and delayed clause normal form transformation.
- A superposition oriented theorem prover
redundancycounterexamplesdeductive inferenceequality eliminationcandidate modelsdirect provabilitydirect rewrite proofrefutationally completestrict superpositionsuperposition without equality factoring
Cited In (8)
- Regular Derivations in Basic Superposition-Based Calculi
- On restrictions of ordered paramodulation with simplification
- Theorem proving in cancellative abelian monoids (extended abstract)
- Harald Ganzinger's legacy: contributions to logics and programming
- Superposition with equivalence reasoning and delayed clause normal form transformation.
- A strict constrained superposition calculus for graphs
- Title not available (Why is that?)
- Superposition with equivalence reasoning and delayed clause normal form transformation
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 Q4249896)