Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Powiadomienia systemowe

Sesja wygasła!

Znaleziono wyników: 4

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: tableaux

Sortuj według:

Ogranicz wyniki do:

Tableau-based translation from first-order logic to modal logic

Perkov Tin, Mikec Luka

Reports on Mathematical Logic

2021

Vol. 56

57--74

We define a procedure for translating a given first-order formula to an equivalent modal formula, if one exists, by using tableau-based bisimulation invariance test. A previously developed tableau procedure tests bisimulation invariance of a given first-order formula, and therefore tests whether that formula is equivalent to the standard translation of some modal formula. Using a closed tableau as the starting point, we show how an equivalent modal formula can be effectively obtained.

An Efficient Tableau Prover using Global Caching for the Description Logic ALC

Nguyen L.A. L.A.

Fundamenta Informaticae

2009

Vol. 93, nr 1-3

273-288

We report on our implementation of a tableau prover for the description logic ALC, which is based on the EXPTIME tableau algorithm using global caching for ALC that was developed jointly by us and Gor´e [9]. The prover, called TGC for "Tableaux with Global Caching", checks satisfiability of a set of concepts w.r.t. a set of global assumptions by constructing an and-or graph, using tableau rules for expanding nodes. We have implemented for TGC a special set of optimizations which co-operates very well with global caching and various search strategies. The test results on the test set T98-sat of DL'98 Systems Comparison indicate that TGC is an efficient prover for ALC. This suggests that global caching together with the set of optimizations used for TGC is worth implementing and experimenting also for other modal/description logics.

On the Influence of Confluence in Modal Logics

Gasquet O.

Fundamenta Informaticae

2006

Vol. 70, nr 3

227-250

In this paper we prove that adding a confluence axiom to a modal logic which behaves rather well from the viewpoint of complexity of the satisfaction problem, drastically increases its complexity and blows it up from PSPACE-completeness to NEXPTIME-completeness. More precisely, we investigate here both monomodal K + confluence and bimodal K with confluence between the two modalities.

Tableaux based decision procedures for modal logics of confluence and density

del Cerro L.F., Gasquet O.

Fundamenta Informaticae

1999

Vol. 40, Nr 4

317-333

In this paper we present a decision procedures for modal logics with transitive models together with additionnal properties like confluence and density. These procedures are tableaux-based, and we show how to handle them in this well-known framework by generalizing usual tableaux (which are trees) to richer structures: directed acyclic graphs.