The following pages link to The TPTP problem library (Q5210777):
Displaying 29 items.
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Clause trees: A tool for understanding and implementing resolution in automated reasoning (Q1402732) (← links)
- Computing answers with model elimination (Q1402748) (← links)
- Proofs as schemas and their heuristic use (Q1583854) (← links)
- Automatic acquisition of search control knowledge from multiple proof attempts. (Q1854367) (← links)
- Efficient model generation through compilation. (Q1854374) (← links)
- Practically useful variants of definitional translations to normal form (Q1854384) (← links)
- Handling transitive relations in first-order automated reasoning (Q2069868) (← links)
- Efficient Well-Definedness Checking (Q3541692) (← links)
- MGTP: A model generation theorem prover — Its advanced features and applications — (Q4610311) (← links)
- Ordered tableaux: Extensions and applications (Q4610325) (← links)
- Subgoal alternation in model elimination (Q4610327) (← links)
- Learning domain knowledge to improve theorem proving (Q4647500) (← links)
- The design of the CADE-13 ATP system competition (Q4647509) (← links)
- SiCoTHEO: Simple competitive parallel theorem provers (Q4647520) (← links)
- The tableau-based theorem prover 3 T A P Version 4.0 (Q4647529) (← links)
- On the practical value of different definitional translations to normal form (Q4647537) (← links)
- Efficient model generation through compilation (Q4647539) (← links)
- Experiments in the heuristic use of past proof experience (Q4647545) (← links)
- Model elimination without contrapositives (Q5210764) (← links)
- The applicability of logic program analysis and transformation to theorem proving (Q5210773) (← links)
- The TPTP problem library (Q5210777) (← links)
- Integration of automated and interactive theorem proving in ILF (Q5234689) (← links)
- ILF-SETHEO (Q5234690) (← links)
- CODE: A powerful prover for problems of condensed detachment (Q5234708) (← links)
- Evolving combinators (Q5234723) (← links)
- Hyper tableaux (Q5235250) (← links)
- Subsumption algorithms based on search trees (Q5878906) (← links)
- Controlled use of clausal lemmas in connection tableau calculi (Q5927985) (← links)
