Cited in
(11)- Splitting through new proposition symbols
- Practical algorithms for deciding path ordering constraint satisfaction.
- Stratified resolution
- Theorem proving in cancellative abelian monoids (extended abstract)
- Harald Ganzinger's legacy: contributions to logics and programming
- FLOTTER
- Induction = I-axiomatization + first-order consistency.
- scientific article; zbMATH DE number 1688812 (Why is no real title available?)
- From search to computation: redundancy criteria and simplification at work
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Automated complexity analysis based on ordered resolution
This page was built for software: Saturate
