lean\(T^ AP\): Lean tableau-based deduction

DOI10.1007/BF00881804zbMath0838.68097OpenAlexW2040816116MaRDI QIDQ1904400

Bernhard Beckert, Joachim Posegga

Publication date: 28 May 1996

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

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

zbMATH Keywords

theorem provingPrologautomated deductionfree-variable semantic tableaux

Mathematics Subject Classification ID

Related Items (30)

HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description) ⋮ MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description) ⋮ Prolog Technology Reinforcement Learning Prover ⋮ From input/output logics to conditional logics via sequents -- with provers ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ CSL-lean: A Theorem-prover for the Logic of Comparative Concept Similarity ⋮ Tableau reasoning for description logics and its extension to probabilities ⋮ The disconnection tableau calculus ⋮ Fifty Years of Prolog and Beyond ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ IeanCOP: lean connection-based theorem proving ⋮ Free variable tableaux for propositional modal logics ⋮ ileanTAP: An intuitionistic theorem prover ⋮ Implementing a relational theorem prover for modal logic ⋮ The disconnection method ⋮ Distributed modal theorem proving with KE ⋮ The tableau-based theorem prover 3 T A P Version 4.0 ⋮ Optimizing proof search in model elimination ⋮ Experimental analysis of some computation rules in a simple parallel reasoning system for the ALC description logic ⋮ Machine learning guidance for connection tableaux ⋮ Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based Approach ⋮ LeanT A P: Lean tableau-based theorem proving ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ leanTAP ⋮ Theorem proving for conditional logics: CondLean and GOALDUCK ⋮ The Tableau Workbench ⋮ Hyper tableaux ⋮ α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic ⋮ Asynchronous knowledge with hidden actions in the situation calculus ⋮ Analytic tableaux for all of \(\mathrm{SIXTEEN}_3\)

Uses Software

• SETHEO
• OTTER
• THOT
• HARP

Cites Work

• Seventy-five problems for testing automatic theorem provers
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• SETHEO: A high-performance theorem prover
• Toward Mechanical Mathematics
• A Mechanical Proof Procedure and its Realization in an Electronic Computer
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: lean\(T^ AP\): Lean tableau-based deduction