swMATH19613MaRDI QIDQ31438FDOQ31438
Author name not available (Why is that?)
Official website: https://github.com/theoremprover-museum/discount
Source code repository: https://github.com/theoremprover-museum/discount
Cited In (60)
- Automatic acquisition of search control knowledge from multiple proof attempts.
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Faster, higher, stronger: E 2.3
- Set of support, demodulation, paramodulation: a historical perspective
- Machine learning for first-order theorem proving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Extensional higher-order paramodulation in Leo-III
- Filter-based resolution principle for lattice-valued propositional logic LP\((X)\)
- Title not available (Why is that?)
- 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
- Robinson arithmetic
- Title not available (Why is that?)
- Learning domain knowledge to improve theorem proving
- 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
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Zipperposition
- Implementing Superposition in iProver (System Description)
- Making higher-order superposition work
- Fine-grained concurrent completion
- Limited resource strategy in resolution theorem proving
- Ordered_Resolution_Prover
- Saturation_Framework
- A comprehensive framework for saturation theorem proving
- Cooperating proof attempts
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
- Integration of automated and interactive theorem proving in ILF
- SAT-Inspired Eliminations for Superposition
- Proving theorems by reuse
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
This page was built for software: DISCOUNT
