Pages that link to "Item:Q1101242"

The following pages link to Seventy-five problems for testing automatic theorem provers (Q1101242):

Displayed 37 items.

• A resolution rule for well-formed formulae (Q808295) ‎ (← links)
• Generating relevant models (Q809621) ‎ (← links)
• Resolution on formula-trees (Q1098648) ‎ (← links)
• A method for simultaneous search for refutations and models by equational constraint solving (Q1198235) ‎ (← links)
• An optimality result for clause form translation (Q1201346) ‎ (← links)
• The value of the four values (Q1274293) ‎ (← links)
• Set theory for verification. I: From foundations to functions (Q1319386) ‎ (← links)
• Accelerating tableaux proofs using compact representations (Q1334905) ‎ (← links)
• Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures (Q1340966) ‎ (← links)
• Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) ‎ (← links)
• The relative complexity of resolution and cut-free Gentzen systems (Q1353988) ‎ (← links)
• Using tactics to reformulate formulae for resolution theorem proving (Q1380410) ‎ (← links)
• IeanCOP: lean connection-based theorem proving (Q1404981) ‎ (← links)
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) ‎ (← links)
• Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500) ‎ (← links)
• lean\(T^ AP\): Lean tableau-based deduction (Q1904400) ‎ (← links)
• The anatomy of vampire. Implementing bottom-up procedures with code trees (Q1904404) ‎ (← links)
• A note on assumptions about Skolem functions (Q1904405) ‎ (← links)
• Avoiding duplicate proofs with the foothold refinement (Q1924821) ‎ (← links)
• Structured proof procedures (Q1924823) ‎ (← links)
• Isabelle's metalogic: formalization and proof checker (Q2055847) ‎ (← links)
• A formalization and proof checker for Isabelle's metalogic (Q2108191) ‎ (← links)
• A prover dealing with nominals, binders, transitivity and relation hierarchies (Q2303237) ‎ (← links)
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) ‎ (← links)
• History and Prospects for First-Order Automated Deduction (Q3454079) ‎ (← links)
• Incremental theory reasoning methods for semantic tableaux (Q4645229) ‎ (← links)
• The disconnection method (Q4645231) ‎ (← links)
• SPASS & FLOTTER version 0.42 (Q4647508) ‎ (← links)
• Exploiting parallelism: highly competitive semantic tree theorem prover (Q4823345) ‎ (← links)
• Increasing the efficiency of automated theorem proving (Q4835513) ‎ (← links)
• Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) ‎ (← links)
• Semantically guided first-order theorem proving using hyper-linking (Q5210771) ‎ (← links)
• The TPTP problem library (Q5210777) ‎ (← links)
• Proving with BDDs and control of information (Q5210793) ‎ (← links)
• LeanT A P: Lean tableau-based theorem proving (Q5210813) ‎ (← links)
• Deciding intuitionistic propositional logic via translation into classical logic (Q5234697) ‎ (← links)
• α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic (Q5504659) ‎ (← links)