Graduate studies at Western
Studia Logica 70 (2):241 - 270 (2002)
|Abstract||Automated theorem proving amounts to solving search problems in usually tremendous search spaces. A lot of research therefore focuses on search space reductions. Our approach reduces the search space which arises when using so-called connection tableau calculi for first-order automated theorem proving. It uses disjunctive constraints over first-order equations to compress certain parts of this search space. We present the basics of our constrained-connection-tableau calculi, a constraint extension of connection tableau calculi, and deal with the efficient handling of constraints during the search process. The new techniques are integrated into the automated connection tableau prover Setheo.|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Riccardo Rosati (2001). A Sound and Complete Tableau Calculus for Reasoning About Only Knowing and Knowing at Most. Studia Logica 69 (1):171-191.
Linh Anh Nguyen & Andrzej Szałas (2011). ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse. Studia Logica 98 (3):387-428.
Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.
Martin Amerbauer (1996). Cut-Free Tableau Calculi for Some Propositional Normal Modal Logics. Studia Logica 57 (2-3):359 - 372.
Wilfried Sieg & John Byrnes (1998). Normal Natural Deduction Proofs (in Classical Logic). Studia Logica 60 (1):67-106.
Mauro Ferrari (1997). Cut-Free Tableau Calculi for Some Intuitionistic Modal Logics. Studia Logica 59 (3):303-330.
Added to index2009-01-28
Total downloads2 ( #246,694 of 739,575 )
Recent downloads (6 months)0
How can I increase my downloads?