Seventy-five problems for testing automatic theorem provers

DOI10.1007/BF02432151zbMath0642.68147OpenAlexW2126583599MaRDI QIDQ1101242

Francis Jeffry Pelletier

Publication date: 1986

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02432151

zbMATH Keywords

automatic theorem proving

Mathematics Subject Classification ID

Related Items

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

Cites Work

• A mechanical solution of Schubert's steamroller by many-sorted resolution
• Schubert's steamroller problem: Formulations and solutions
• The complexity of Gentzen systems for propositional logic
• Computer proofs of limit theorems
• Breadth-first search: some surprising results
• On the paradox of grounded classes
• Hard examples for resolution
• Problems and Experiments for and with Automated Theorem-Proving Programs
• On Resolution with Clauses of Bounded Size
• The relative efficiency of propositional proof systems
• On Tarski's formalization of predicate logic with identity