Wyniki wyszukiwania - BazTech

1

An Improved Set-based Reasoner for the Description Logic 𝒟ℒD4,×

Cantone Domenico, Nicolosi-Asmundo Marianna, Santamaria Daniele Francesco

Fundamenta Informaticae

|

2021

|

Vol. 178, nr 4

315--346

EN

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic 𝒟ℒ〈4LQSR,×〉(D ) (𝒟 ℒD 4,×, for short). Our application solves the main TBox and ABox reasoning problems for 𝒟 ℒ D 4,×. In particular, it solves the consistency and the classification problems for 𝒟 ℒD 4,× -knowledge bases represented in set-theoretic terms, and a generalization of the Conjunctive Query Answering problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and improves a previous version, is implemented in C++. It supports 𝒟 ℒ D 4,×-knowledge bases serialized in the OWL/XML format and it admits also rules expressed in SWRL (Semantic Web Rule Language).

2

An ExpTime Tableau Method for Dealing with Nominals and Qualified Number Restrictions in Deciding the Description Logic SHOQ

Nguyen L. A., Golińska-Pilarek J.

Fundamenta Informaticae

|

2014

|

Vol. 135, nr 4

433--449

EN

We present the first tableau method with an EXPTIME (optimal) complexity for checking satisfiability of a knowledge base in the description logic SHOQ, which extends ALC with transitive roles, hierarchies of roles, nominals and qualified number restrictions. The complexity is measured using unary representation for numbers (in number restrictions). Our procedure is based on global caching and integer linear feasibility checking.

3

Analiza tablic decyzyjnych z wykorzystaniem monotonicznego rachunku sekwensów

Tkacz J., Adamski M.

Przegląd Elektrotechniczny

|

2013

|

R. 89, nr 6

256--259

PL

W artykule przedstawiono nowatorski sposób analizy systemów regułowych z wykorzystaniem symbolicznego wnioskowania w monotonicznej logice sekwentów Gentzena. Badany system dyskretny jest opisywany w postaci tablicy decyzyjnej. Celem analizy systemu jest usunięcie zbytecznych kolumn w tablicy decyzyjnej oraz nieistotnych symboli zmiennych logicznych w jej poszczególnych wierszach. Efektywny aparat wnioskowania w logice formalnej umożliwia sprawne wyznaczanie transwersal krawędzi hipergrafu rozróżnialności.

EN

The paper presents a new methodology for symbolic reduction of multivalued decision tables, currently intensively used for compact behavioral specifications of logic controllers. As an example the well known problem of simplification of a set of several logic rules with many variables is chosen. As a completely new, original solution, the formal automated reasoning based on Gentzen propositional calculus together with hypergraph theory are jointly used. The clique-transversal symbolic calculation is performed by means of effective reasoning in Gentzen calculus.

4

Redukcja binarnych tablic decyzyjnych z wykorzystaniem automatycznego wnioskowania

Adamski M., Tkacz J., Wrzesińska B.

Metody Informatyki Stosowanej

|

2010

|

nr 3 (24)

5-12

PL

W artykule przedstawiono sposób redukcji binarnych tablic decyzyjnych z wykorzystaniem systemu komputerowego dowodzenia twierdzeń w zdaniowym rachunku Gentzena [1, 4]. Binarna tablica decyzyjna przedstawia słabo określoną funkcję logiczną wielu zmiennych [6, 7]. Przykładową tablicę zaczerpnięto z książki [5], ze względu na zamieszczony w niej pełny i systematyczny opis wszystkich kroków minimalizacji funkcji i stopniowo uzyskiwanych rezultatów częściowych. Proponowany sposób minimalizacji symbolicznej postaci funkcji logicznej umożliwia w stosunkowo sprawny sposób otrzymywanie rezultatów dokładnych, wraz z formalnym dowodem ich gwarantowanej poprawności.

EN

The paper presents a new methodology for symbolic reduction of binary decision tables, currently intensively used for compact behavioral specifications of logic controllers. As an example the well known problem of simplification of a set of boolean relations with many variables and large sets of don’t care condition is chosen. They described also a special class of Boolean function called weakly specified or strongly unspecified. As a completely new, original solution, the formal automated reasoning based on Gentzen propositional calculus together with hypergraph theory are jointly used. The clique-transversal symbolic calculation is performed by means of effective reasoning in Gentzen calculus, giving the formal proof of all transformations.

5

An Empirical Study of QBF Encodings: from Treewidth Estimation to Useful Preprocessing

Pulina L., Tacchella A.

Fundamenta Informaticae

|

2010

|

Vol. 102, nr 3/4

391-427

EN

From an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide about the truth of formulas given limited computational resources. In this paper, we start from the problem of computing empirical hardness markers, i.e., features that can discriminate between hard and easy QBFs, and we end up showing that such markers can be useful to improve our understanding of QBF preprocessors. In particular, considering the connection between classes of tractable QBFs and the treewidth of associated graphs, we show that (an approximation of) treewidth is indeed a marker of empirical hardness and it is the only parameter which succeeds consistently in being so, even considering several other purely syntactic candidates which have been successfully employed to characterize QBFs in other contexts. We also show that treewidth approximations can be useful to describe the effect of QBF preprocessors, in that some QBF solvers benefit from a preprocessing phase when it reduces the treewidth of their input. Our experiments suggest that structural simplifications reducing treewidth are a potential enabler for the solution of hard QBF encodings.

6

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

EN

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.

7

Non-Clausal Reasoning with Definite Theories

Stachniak Z.

Fundamenta Informaticae

|

2001

|

Vol. 48, nr 4

363-388

EN

In this paper we propose a general-purpose first-order automated reasoning framework based on the notion of a definite formula and on a non-clausal variant of SLD-resolution. This framework provides a universal Horn clause-like representation of knowledge for classical as well as a range of non-classical first-order logics. It provides a resolution-style method for automated reasoning with theories of definite formulas.