DISCOUNT

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