DISCOUNT
From MaRDI portal
Cited in
(60)- Automatic acquisition of search control knowledge from multiple proof attempts.
- Faster, higher, stronger: E 2.3
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Set of support, demodulation, paramodulation: a historical perspective
- Machine learning for first-order theorem proving
- scientific article; zbMATH DE number 2043541 (Why is no real title available?)
- scientific article; zbMATH DE number 1882065 (Why is no real title available?)
- Filter-based resolution principle for lattice-valued propositional logic LP(X)
- Extensional higher-order paramodulation in Leo-III
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Performance of clause selection heuristics for saturation-based theorem proving
- Octopus: combining learning and parallel search
- A comprehensive framework for saturation theorem proving
- Making higher-order superposition work
- Superposition with lambdas
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- PLAGIATOR
- TGTP
- OTTER
- StarExec
- iProver
- PARTHEO
- Octopus
- Roo
- HOT
- EQP
- CLIN
- SNARK
- Waldmeister
- Angelic Verification
- HERBY
- SPTHEO
- Peers-mcd
- Scavenger
- PARTHENON
- Aquarius
- AVATAR
- Logtk
- KoMeT
- Lambda Free RPOs
- Nested Multisets
- FLOTTER
- Zipperposition
- Ordered_Resolution_Prover
- Saturation_Framework
- Learning domain knowledge to improve theorem proving
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Implementing Superposition in iProver (System Description)
- Limited resource strategy in resolution theorem proving
- Making higher-order superposition work
- Fine-grained concurrent completion
- A comprehensive framework for saturation theorem proving
- Cooperating proof attempts
- \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Integration of automated and interactive theorem proving in ILF
- SAT-Inspired Eliminations for Superposition
- Proving theorems by reuse
- Robinson arithmetic
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
This page was built for software: DISCOUNT
