Name
Abstract | ||
|---|---|---|
In this work a tableau calculus is proposed, that checks whether a finite set of formulae in propositional linear temporal logic (LTL) has a finite model whose cardinality is bounded by a constant given in input, and constructs such a model, if any. From a theoretical standpoint, the method can also be used to check finite satisfiability tout court. The following properties of the proposed calculus are proved: termination, soundness and completeness w.r.t. finite model construction. The motivation behind this work is the design of a logical language to model planning problems and an associated calculus for plan construction, integrating the declarativity, expressiveness and flexibility typical of the logical languages with the capability of embedding search-based techniques well established in the planning community. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/3-540-69778-0_18 | TABLEAUX |
Keywords | Field | DocType |
logical language,linear temporal logic,plan construction,finite satisfiability,finite model,associated calculus,bounded model search,proposed calculus,tableau calculus,finite model construction,planning community,finite set | Computer science,Cardinality,Algorithm,Propositional calculus,Linear temporal logic,Modal logic,Soundness,Temporal logic,Completeness (statistics),Bounded function | Conference |
Volume | ISSN | ISBN |
1397 | 0302-9743 | 3-540-64406-7 |
Citations | PageRank | References |
12 | 0.69 | 16 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Serenella Cerrito | 1 | 139 | 13.72 |
| Marta Cialdea Mayer | 2 | 274 | 28.25 |