DISCOUNT

swMATH19613MaRDI QIDQ31438FDOQ31438

Author name not available (Why is that?)

Source code repository: https://github.com/theoremprover-museum/discount

Cited In (30)

• 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
• Cooperating Proof Attempts
• Machine learning for first-order theorem proving
• Title not available (Why is that?)
• Title not available (Why is that?)
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Extensional higher-order paramodulation in Leo-III
• Filter-based resolution principle for lattice-valued propositional logic LP\((X)\)
• Title not available (Why is that?)
• Octopus: combining learning and parallel search
• A comprehensive framework for saturation theorem proving
• Making higher-order superposition work
• Superposition with lambdas
• Title not available (Why is that?)
• Learning domain knowledge to improve theorem proving
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• Citius altius fortius
• Implementing Superposition in iProver (System Description)
• Making higher-order superposition work
• Fine-grained concurrent completion
• Limited resource strategy in resolution theorem proving
• A comprehensive framework for saturation theorem proving
• 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

This page was built for software: DISCOUNT