Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic.
|
CADE |
2023 |
0 |
Efficient Local Reductions to Basic Modal Logic.
|
CADE |
2021 |
5 |
KSP: A Resolution-based Prover for Multimodal K, Abridged Report.
|
IJCAI |
2017 |
13 |
Theorem Proving for Metric Temporal Logic over the Naturals.
|
CADE |
2017 |
10 |
A Modal-Layered Resolution Calculus for K.
|
TABLEAUX |
2015 |
14 |
Ordered Resolution for Coalition Logic.
|
TABLEAUX |
2015 |
2 |
Fair Derivations in Monodic Temporal Reasoning.
|
CADE |
2009 |
9 |
A Refined Resolution Calculus for CTL.
|
CADE |
2009 |
13 |
Automated Reasoning About Metric and Topology.
|
JELIA |
2006 |
10 |
Deciding Monodic Fragments by Temporal Resolution.
|
CADE |
2005 |
14 |
Data Complexity of Reasoning in Very Expressive Description Logics.
|
IJCAI |
2005 |
266 |
Reducing SHIQ-Description Logic to Disjunctive Datalog Programs.
|
KR |
2004 |
278 |
Reasoning in Description Logics with a Concrete Domain in the Framework of Resolution.
|
ECAI |
2004 |
39 |
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi.
|
LPAR |
2004 |
0 |
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae.
|
CADE |
2003 |
41 |
TRP++2.0: A Temporal Resolution Prover.
|
CADE |
2003 |
75 |
A New Clausal Class Decidable by Hyperresolution.
|
CADE |
2002 |
24 |
Scientific Benchmarking with Temporal Logic Decision Procedures.
|
KR |
2002 |
36 |
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae.
|
LPAR |
2001 |
19 |
MSPASS: Modal Reasoning by Translation and First-Order Resolution.
|
TABLEAUX |
2000 |
96 |
A Resolution Decision Procedure for Fluted Logic.
|
CADE |
2000 |
23 |
Maslov's Class K Revisited.
|
CADE |
1999 |
31 |
On the Relation of Resolution and Tableaux Proof Systems for Description Logics.
|
IJCAI |
1999 |
38 |
Simplification and Backjumping in Modal Tableau.
|
TABLEAUX |
1998 |
28 |
On Evaluating Decision Procedures for Modal Logic.
|
IJCAI |
1997 |
94 |