α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic

DOI10.1007/978-3-540-89982-2_26zbMath1183.68561OpenAlexW1484198662MaRDI QIDQ5504659

William Byrd, Joseph P. Near, Daniel P. Friedman

Publication date: 22 January 2009

Published in: Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-89982-2_26

Mathematics Subject Classification ID

Related Items (2)

Nominal syntax with atom substitutions ⋮ Nominal equational problems

Uses Software

• TPTP
• SATCHMO
• Twelf
• leanTAP
• aleanTAP
• miniKanren
• KANREN

Cites Work

• Seventy-five problems for testing automatic theorem provers
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• The TPTP problem library. CNF release v1. 2. 1
• Nominal unification
• lean\(T^ AP\): Lean tableau-based deduction
• Backtracking, interleaving, and terminating monad transformers
• Automated reasoning with a constraint-based metainterpreter
• Logic Programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic