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