Name
Abstract | ||
|---|---|---|
Ordered fine-grained resolution with selection is a sound and complete resolution-based calculus for monodic first-order temporal logic. The inference rules of the calculus are based on standard resolution between different types of temporal clauses on one hand and inference rules with semi-decidable applicability conditions that handle eventualities on the other hand. In this paper we illustrate how the combination of these two different types of inference rules can lead to unfair derivations in practice. We also present an inference procedure that allows us to construct fair derivations and prove its refutational completeness. We conclude with some experimental results obtained with the implementation of the new procedure in the theorem prover TSPASS. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02959-2_21 | CADE |
Keywords | Field | DocType |
ordered fine-grained resolution,monodic first-order temporal logic,monodic temporal reasoning,temporal clause,new procedure,fair derivations,inference procedure,different type,complete resolution-based calculus,inference rule,standard resolution,theorem prover | Discrete mathematics,Inference,Computer science,Automated theorem proving,Proof calculus,Algorithm,Temporal logic,Rule of inference,Completeness (statistics) | Conference |
Volume | ISSN | Citations |
5663 | 0302-9743 | 5 |
PageRank | References | Authors |
0.44 | 13 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michel Ludwig | 1 | 113 | 7.67 |
| Ullrich Hustadt | 2 | 1007 | 66.68 |