leanT^ AP: Lean tableau-based deduction
From MaRDI portal
Lean\(T^ AP\): Lean tableau-based deduction
Recommendations
- LeanT A P: Lean tableau-based theorem proving
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- scientific article; zbMATH DE number 1341478
- Logic programming as a basis for lean automated deduction
- The Lean theorem prover (system description)
- IeanCOP: lean connection-based theorem proving
- scientific article; zbMATH DE number 1956546
- A tableau calculus for minimal model reasoning
- scientific article; zbMATH DE number 1292293
Cites work
- A Mechanical Proof Procedure and its Realization in an Electronic Computer
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- scientific article; zbMATH DE number 46359 (Why is no real title available?)
- scientific article; zbMATH DE number 48763 (Why is no real title available?)
- scientific article; zbMATH DE number 1292302 (Why is no real title available?)
- scientific article; zbMATH DE number 517067 (Why is no real title available?)
- SETHEO: A high-performance theorem prover
- Seventy-five problems for testing automatic theorem provers
- Toward Mechanical Mathematics
Cited in
(37)- IeanCOP: lean connection-based theorem proving
- Tableau reasoning for description logics and its extension to probabilities
- Machine learning guidance for connection tableaux
- From input/output logics to conditional logics via sequents -- with provers
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
- leanTAP
- Asynchronous knowledge with hidden actions in the situation calculus
- Analytic tableaux for all of \(\mathrm{SIXTEEN}_3\)
- nanoCoP: a non-clausal connection prover
- Implementing a relational theorem prover for modal logic K
- Experimental analysis of some computation rules in a simple parallel reasoning system for the \(\mathcal{ALC}\) description logic
- CSL-\textsf{lean}: a theorem-prover for the logic of comparative concept similarity
- Theorem proving for conditional logics: CondLean and GOALDUCK
- Lean induction principles for tableaux
- Free variable tableaux for propositional modal logics
- \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
- 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
- Probabilistic DL reasoning with pinpointing formulas: a Prolog-based approach
- The Tableau Workbench
- 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
- LeanT A P: Lean tableau-based theorem proving
- Hyper tableaux
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Fifty Years of Prolog and Beyond
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- A Mizar mode for HOL
- A tableau system for first-order logic with standard names
- Sequent calculi and an efficient theorem prover for conditional logics with selection function semantics
- The HOL-CSP Refinement Toolkit
- HOL-CSP Version 2.0
- A Sound Type System for Physical Quantities, Units, and Measurements
- The disconnection tableau calculus
This page was built for publication: lean\(T^ AP\): Lean tableau-based deduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1904400)
