Hide abstracts BibTeX entries  
2021  
[52] 
2021. Rough set reasoning using answer set programs. International Journal of Approximate Reasoning, 130(March):126–149. Elsevier. DOI: 10.1016/j.ijar.2020.12.010. Note: Funding: ELLIIT Network Organization for Information and Communication Technology, Sweden; Swedish Foundation for Strategic Research SSF(Smart Systems Project) [RIT150097]; Jinan University (Zhuhai Campus); National Science Centre PolandNational Science Centre, Poland [2017/27/B/ST6/02018] Fulltext: https://doi.org/10.1016/j.ijar.2020.12.0... fulltext:print: http://liu.divaportal.org/smash/get/div... Reasoning about uncertainty is one of the main cornerstones of Knowledge Representation. Formal representations of uncertainty are numerous and highly varied due to different types of uncertainty intended to be modeled such as vagueness, imprecision and incompleteness. There is a rich body of theoretical results that has been generated for many of these approaches. It is often the case though, that pragmatic tools for reasoning with uncertainty lag behind this rich body of theoretical results. Rough set theory is one such approach for modeling incompleteness and imprecision based on indiscernibility and its generalizations. In this paper, we provide a pragmatic tool for constructively reasoning with generalized rough set approximations that is based on the use of Answer Set Programming (Asp). We provide an interpretation of answer sets as (generalized) approximations of crisp sets (when possible) and show how to use Asp solvers as a tool for reasoning about (generalized) rough set approximations situated in realistic knowledge bases. The paper includes generic Asp templates for doing this and also provides a case study showing how these techniques can be used to generate reducts for incomplete information systems. Complete, ready to run clingo Asp code is provided in the Appendix, for all programs considered. These can be executed for validation purposes in the clingo Asp solver. 
.

2020  
[51] 
2020. On the Probability and Cost of Ignorance, Inconsistency, Nonsense and More. Journal of MultipleValued Logic and Soft Computing, 34(56):423–450. Old City Publishing. Note: Funding agencies: National Science Centre PolandNational Science Center, PolandNational Science Centre, Poland [2017/27/B/ST6/02018] Journal home page: https://www.oldcitypublishing.com/journa... Ignorance, inconsistency, nonsense and similar phenomena are omnipresent in everyday reasoning. They have been intensively studied, especially in the area of multiplevalued logics. Therefore we develop a framework for belief bases, combining multiplevalued and probabilistic reasoning, with the main focus on the way belief bases are actually used and accessed through queries.As an implementation tool we use a probabilistic programming language PROBLOG. Though based on distribution semantics with the independence assumption, we show how its constructs can successfully be used in implementing the considered logics and belief bases. In particular, we develop a technique for shifting probabilistic dependencies to the level of symbolic parts of belief bases.We also discuss applications of the framework in reasoning with Likerttype scales, widely exploited in questionnairebased experimental research in psychology, economics, sociology, politics, public opinion measurements, and related areas. 
.

[50] 
2020. A Paraconsistent ASPlike Language with Tractable Model Generation. Journal of Applied Logics  IfCoLog Journal of Logic and Applications, 7(3):361–389. College Publications. Note: Funding agencies: This work has been supported by grant 2017/27/B/ST6/02018 of the National Science Centre Poland. Link to article: http://www.collegepublications.co.uk/dow... fulltext:print: http://liu.divaportal.org/smash/get/div... Answer Set Programming (ASP) is nowadays a dominant rulebased knowledge representation tool. Though existing ASP variants enjoy efficient implementations, generating an answer set remains intractable. The goal of this research is to define a new ASPlike rule language, 4SP, with tractable model generation. The language combines ideas of ASP and a paraconsistent rule language 4QL. Though 4SP shares the syntax of ASP and for each program all its answer sets are among 4SP models, the new language differs from ASP in its logical foundations, the intended methodology of its use and complexity of computing models. As we show in the paper, 4QL can be seen as a paraconsistent counterpart of ASP programs stratified with respect to default negation. Although model generation for 4QL programs is tractable, dropping stratification makes it intractable for both 4QL and ASP. To retain tractability while allowing nonstratified programs, in 4SP we introduce trial expressions interlacing programs with hypotheses as to the truth values of default negations. This allows us to develop a model generation algorithm with deterministic polynomial time complexity. We also show relationships among 4SP, ASP and 4QL. 
.

2019  
[49] 
2019. A paraconsistent approach to actions in informationally complex environments. Annals of Mathematics and Artificial Intelligence, 86(4):231–255. SPRINGER. DOI: 10.1007/s10472019096279. Note: Funding AgenciesPolish National Science Centre [2015/19/B/ST6/02589]; ELLIIT Network Organization for Information and Communication Technology; Swedish Foundation for Strategic Research FSR (SymbiKBot Project) fulltext:print: http://liu.divaportal.org/smash/get/div... Contemporary systems situated in realworld open environments frequently have to cope with incomplete and inconsistent information that typically increases complexity of reasoning and decision processes. Realistic modeling of such informationally complex environments calls for nuanced tools. In particular, incomplete and inconsistent information should neither trivialize nor stop both reasoning or planning. The paper introduces ACTLOG, a rulebased fourvalued language designed to specify actions in a paraconsistent and paracomplete manner. ACTLOG is an extension of 4QL(Bel), a language for reasoning with paraconsistent belief bases. Each belief base stores multiple world representations. In this context, ACTLOGs action may be seen as a belief bases transformer. In contrast to other approaches, ACTLOG actions can be executed even when the underlying belief base contents is inconsistent and/or partial. ACTLOG provides a nuanced action specification tools, allowing for subtle interplay among various forms of nonmonotonic, paraconsistent, paracomplete and doxastic reasoning methods applicable in informationally complex environments. Despite its rich modeling possibilities, it remains tractable. ACTLOG permits for composite actions by using sequential and parallel compositions as well as conditional specifications. The framework is illustrated on a decontamination case study known from the literature. 
.

[48] 
2019. Paraconsistent Reasoning in Cops and Robber Game with Uncertain Information: A SimulationBased Analysis. International Journal of Uncertainty Fuzziness and KnowledgeBased Systems, 27(3):429–455. WORLD SCIENTIFIC PUBL CO PTE LTD. DOI: 10.1142/S021848851950020X. Note: Funding AgenciesPolish National Science Centre [2012/05/B/ST6/03094, 2015/19/B/ST6/02589] We apply a nonclassical fourvalued logic in the process of reasoning regarding strategies for cops in a modified game of \"Cops and Robber\" played on a graph. We extend the game by introducing uncertainty in a form of random failures of detecting devices. This is realized by allowing that a robber can be detected in a node only with the given probability PA. Additionally, with the probability PF, cops can be given a falsepositive, i.e., they are informed that the robber is located at some node, whereas it is located somewhere else. Consequently, nonzero PF introduces a measurement noise into the system. All the cops have access to information provided by the detectors and can communicate with each other, so they can coordinate the search. By adjusting the number of detectors,PA, and PF we can achieve a smooth transition between the two wellknown variants of the game: \"with fully visible robber\" and \"with invisible robber\". We compare a simple probabilistic strategy for cops with the nonparametric strategy based on reasoning with a fourvalued paraconsistent logic. It is shown that this novel approach leads to a good performance, as measured by the required mean catchtime. We conclude that this type of reasoning can be applied in realworld applications where there is no knowledge about the underlying source of errors which is particularly useful in robotics. 
.

2018  
[47] 
2018. Paraconsistent RuleBased Reasoning with Graded Truth Values. Modern artificial systems, such as cooperative traffic systems or swarm robotics, are made of multiple autonomous agents, each handling uncertain, partial and potentially inconsistent information, used in their reasoning and decision making. Graded reasoning, being a suitable tool for addressing phenomena related to such circumstances, is investigated in the literature in many contexts – from graded modal logics to various forms of approximate reasoning. In this paper we first introduce a family of manyvalued paraconsistent logics parametrised by a number of truth/falsity/inconsistency grades allowing one to handle multiple truthvalues at the desired level of accuracy. Second, we define a corresponding family of rulebased languages with graded truthvalues as firstclass citizens, enjoying tractable query evaluation. In addition, we introduce introspection operators allowing one to resolve inconsistencies and/or lack of information in a nonmonotonic manner. We illustrate and discuss the use of the framework in an autonomous robot scenario. 
.

2015  
[46] 
2015. Towards richer rule languages with polynomial data complexity for the Semantic Web. Data & Knowledge Engineering, 9697(??):57–77. ELSEVIER SCIENCE BV. DOI: 10.1016/j.datak.2015.04.005. We introduce a Horn description logic called HornDL, which is strictly and essentially richer than HornReg(1), HornSHTQ and HornSROIQ, while still has PTime data complexity. In comparison with HornSROIQ, HornDL additionally allows the universal role and assertions of the form irreflexive(s), s(a, b), a b. More importantly, in contrast to all the wellknown Horn fragments epsilon L, DLLite, DLP, HornSHIQ, and HornSROIQ of description logics, HornDL allows a form of the concept constructor \"universal restriction\" to appear at the left hand side of terminological inclusion axioms. Namely, a universal restriction can be used in such places in conjunction with the corresponding existential restriction. We develop the first algorithm with PTime data complexity for checking satisfiability of HornDL knowledge bases. 
.

[45] 
2015. Paraconsistent semantics of speech acts. This paper discusses an implementation of four speech acts: assert, concede, request and challenge in a paraconsistent framework. A natural fourvalued model of interaction yields multiple new cognitive situations. They are analyzed in the context of communicative relations, which partially replace the concept of trust. These assumptions naturally lead to six types of situations, which often require performing conflict resolution and belief revision. The particular choice of a rulebased, DATALOC. like query language 4QL as a fourvalued implementation framework ensures that, in contrast to the standard twovalued approaches, tractability of the model is achieved. 
.

2014  
[44] 
2014. A Horn Fragment with PTime Data Complexity of Regular Description Logic with Inverse. VNU Journal of Computer Science and Communication Engineering, 30(4):14–28. Link to publication: http://www.jcsce.vnu.edu.vn/index.php/jc... We study a Horn fragment called HornRegI of the regular description logic with inverse RegI, which extends the description logic ALC with inverse roles and regular role inclusion axioms characterized by finite automata. In contrast to the wellknown Horn fragments EL, DLLite, DLP, HornSHIQ and HornSROIQ of description logics, HornRegI allows a form of the concept constructor \"universal restriction\" to appear at the left hand side of terminological inclusion axioms, while still has PTIME data complexity. Namely, a universal restriction can be used in such places in conjunction with the corresponding existential restriction. We provide an algorithm with PTIME data complexity for checking satisfiability of HornRegI knowledge bases. 
.

[43] 
2014. WORL: a nonmonotonic rule language for the semantic web. We develop a new Web ontology rule language, called WORL, which combines a variant of OWL 2 RL with eDatalog ¬ . We allow additional features like negation, the minimal number restriction and unary external checkable predicates to occur at the lefthand side of concept inclusion axioms. Some restrictions are adopted to guarantee a translation into eDatalog ¬ . We also develop the wellfounded semantics and the stable model semantics for WORL as well as the standard semantics for stratified WORL (SWORL) via translation into eDatalog ¬ . Both WORL with respect to the wellfounded semantics and SWORL with respect to the standard semantics have PTime data complexity. In contrast to the existing combined formalisms, in WORL and SWORL negation in concept inclusion axioms is interpreted using nonmonotonic semantics. 
.

2013  
[42] 
2013. Automated Generation of Logical Constraints on Approximation Spaces Using Quantifier Elimination. Fundamenta Informaticae, 127(14):135–149. IOS Press. DOI: 10.3233/FI2013900. Note: Funding AgenciesSwedish Research Council (VR) Linnaeus Center CADICSELLIIT Excellence Center at LinkopingLund in Information TechnologyCUAS projectSSF, the Swedish Foundation for Strategic Research This paper focuses on approximate reasoning based on the use of approximation spaces. Approximation spaces and the approximated relations induced by them are a generalization of the rough setbased approximations of Pawlak. Approximation spaces are used to define neighborhoods around individuals and rough inclusion functions. These in turn are used to define approximate sets and relations. In any of the approaches, one would like to embed such relations in an appropriate logical theory which can be used as a reasoning engine for specific applications with specific constraints. We propose a framework which permits a formal study of the relationship between properties of approximations and properties of approximation spaces. Using ideas from correspondence theory, we develop an analogous framework for approximation spaces. We also show that this framework can be strongly supported by automated techniques for quantifier elimination. 
.

[41] 
2013. How an agent might think. Logic journal of the IGPL (Print), 21(3):515–535. Oxford University Press (OUP): Policy A  Oxford Open Option A. DOI: 10.1093/jigpal/jzs051. The current article is devoted to extensions of the rule query language 4QL proposed by Małuszyński and Szałas. 4QL is a Datalog<sup>¬¬</sup>like language, allowing one to use rules with negation in heads and bodies of rules. It is based on a simple and intuitive semantics and provides uniform tools for lightweight versions of wellknown forms of nonmonotonic reasoning. In addition, 4QL is tractable w.r.t. data complexity and captures PTime queries. In the current article we relax most of restrictions of 4QL, obtaining a powerful but still tractable query language 4QL<sup>+</sup>. In its development we mainly focused on its pragmatic aspects: simplicity, tractability and generality. In the article we discuss our approach and choices made, define a new, more general semantics and investigate properties of 4QL<sup>+</sup>. 
.

2011  
[40] 
2011. ConversePDL with Regular Inclusion Axioms: A Framework for MAS Logics. <em>In this paper we study automated reasoning in the modal logic CPDLreg which is a combination of CPDL (Propositional Dynamic Logic with Converse) and REGc (Regular Grammar Logic with Converse). The logic CPDL is widely used in many areas, including program verification, theory of action and change, and knowledge representation. On the other hand, the logic REGc is applicable in reasoning about epistemic states and ontologies (via Description Logics). The modal logic CPDLreg can serve as a technical foundation for reasoning about agency. Even very rich multiagent logics can be embedded into CPDLreg via a suitable translation. Therefore, CPDLreg can serve as a test bed to implement and possibly verify new ideas without providing specific automated reasoning techniques for the logic in question. This process can to a large extent be automated. The idea of embedding various logics into CPDLreg is illustrated on a rather advanced logic TEAMLOGK designed to specify teamwork in multiagent systems. Apart from defining informational and motivational attitudes of groups of agents, TEAMLOGK allows for grading agents' beliefs, goals and intentions. The current paper is a companion to our paper (DuninKęplicz et al., 2010a). The main contribution are proofs of soundness and completeness of the tableau calculus for CPDLreg provided in (DuninKęplicz et al., 2010a).</em> 
.

[39] 
2011. ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse. Studia Logica: An International Journal for Symbolic Logic, 98(3):387–428. Springer Berlin/Heidelberg. DOI: 10.1007/s1122501193413. Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse (<em>REG</em> <sup><em>c</em> </sup>logics) and present sound and complete tableau calculi for the general satisfiability problem of <em>REG</em> <sup><em>c</em> </sup>logics and the problem of checking consistency of an ABox w.r.t. a TBox in a <em>REG</em> <sup><em>c</em> </sup>logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to which various optimization techniques can be applied. We also prove a new result that the data complexity of the instance checking problem in <em>REG</em> <sup><em>c</em></sup>logics is coNPcomplete. 
.

[38] 
2011. Logical Foundations and Complexity of 4QL, a Query Language with Unrestricted Negation. The paper discusses properties of 4QL, a DATALOG¬¬like query language, originally outlined by Małuszy´nski and Szałas (Małuszy´nski & Szałas, 2011). 4QL allows one to use rules with negation in heads and bodies of rules. It is based on a simple and intuitive semantics and provides uniform tools for “lightweight” versions of known forms of nonmonotonic reasoning. Negated literals in heads of rules may naturally lead to inconsistencies. On the other hand, rules do not have to attach meaning to some literals. Therefore 4QL is founded on a fourvalued semantics, employing the logic introduced in (Małuszy´nski et al., 2008; Vitória et al., 2009) with truth values: ‘true’, ‘false’, ‘inconsistent’ and ‘unknown’. In addition, 4QL is tractable w.r.t. data complexity and captures PTIME queries. Even though DATALOG¬¬ is known as a concept for the last 30 years, to our best knowledge no existing approach enjoys these properties. In the current paper we:<ul><li>investigate properties of wellsupported models of 4QL</li><li>prove the correctness of the algorithm for computing wellsupported models</li><li>show that 4QL has PTIME data complexity and captures PTIME.</li></ul> 
.

2010  
[37] 
2010. Tableaux with Global Caching for Checking Satisfiability of a Knowledge Base in the Description Logic SH. Transactions on Computational Collective Intelligence, 1(1):21–38. Springer. ISBN: 9783642150333. DOI: 10.1007/9783642150340_2. Description logics (DLs) are a family of knowledge representation languages which can be used to represent the terminological knowledge of an application domain in a structured and formally wellunderstood way. DLs can be used, for example, for conceptual modeling or as ontology languages. In fact, OWL (Web Ontology Language), recommended by W3C, is based on description logics. In the current paper we give the first direct ExpTime (optimal) tableau decision procedure, which is not based on transformation or on the precompletion technique, for checking satisfiability of a knowledge base in the description logic <em>SH</em><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char53.png\" /><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char48.png\" />. Our procedure uses sound global caching and can be implemented as an extension of the highly optimized tableau prover TGC to obtain an efficient program for the mentioned satisfiability problem. 
.

[36] 
2010. Checking Consistency of an ABox w.r.t. Global Assumptions in PDL. We reformulate Pratts tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and its implementation is more direct. Extending the method we give the first Ex PT m E (optimal) tableau decision procedure not based on transformation for checking consistency of an ABox w.r.t. a TBox in PDL (here, PDL is treated as a description logic). We also prove a new result that the data complexity of the instance checking problem in PDL is coNPcomplete. 
.

[35] 
2010. A Framework for Graded Beliefs, Goals and Intentions. In natural language we often use graded concepts, reflecting different intensity degrees of certain features. Whenever such concepts appear in a given reallife context, they need to be appropriately expressed in its models. In this paper, we provide a framework which allows for extending the BGI model of agency by grading beliefs, goals and intentions. We concentrate on TEAMLOG [6, 7, 8, 9, 12] and provide a complexityoptimal decision method for its graded version TEAMLOG(K) by translating it into CPDLreg (propositional dynamic logic with converse and \"inclusion axioms\" characterized by regular languages). We also develop a tableau calculus which leads to the first EXPTIME (optimal) tableau decision procedure for CPDLreg. As CPDLreg is suitable for expressing complex properties of graded operators, the procedure can also be used as a decision tool for other multiagent formalisms. 
.

[34] 
2010. A Layered RuleBased Architecture for Approximate Knowledge Fusion. COMPUTER SCIENCE AND INFORMATION SYSTEMS, 7(3):617–642. COMSIS CONSORTIUM. DOI: 10.2298/CSIS100209015D. In this paper we present a framework for fusing approximate knowledge obtained from various distributed, heterogenous knowledge sources. This issue is substantial in modeling multiagent systems, where a group of loosely coupled heterogeneous agents cooperate in achieving a common goal. In paper [5] we have focused on defining general mechanism for knowledge fusion. Next, the techniques ensuring tractability of fusing knowledge expressed as a Horn subset of propositional dynamic logic were developed in [13,16]. Propositional logics may seem too weak to be useful in realworld applications. On the other hand, propositional languages may be viewed as sublanguages of firstorder logics which serve as a natural tool to define concepts in the spirit of description logics [2]. These notions may be further used to define various ontologies, like e. g. those applicable in the Semantic Web. Taking this step, we propose a framework, in which our Horn subset of dynamic logic is combined with deductive database technology. This synthesis is formally implemented in the framework of HSPDL architecture. The resulting knowledge fusion rules are naturally applicable to realworld data. 
.

[33] 
2010. Tractable approximate knowledge fusion using the Horn fragment of serial propositional dynamic logic. International Journal of Approximate Reasoning, 51(3):346–362. Elsevier. DOI: 10.1016/j.ijar.2009.11.002. In this paper we investigate a technique for fusing approximate knowledge obtained from distributed, heterogeneous information sources. This issue is substantial, e.g., in modeling multiagent systems, where a group of loosely coupled heterogeneous agents cooperate in achieving a common goal. Information exchange, leading ultimately to knowledge fusion, is a natural and vital ingredient of this process. We use a generalization of rough sets and relations [30], which depends on allowing arbitrary similarity relations. The starting point of this research is [6], where a framework for knowledge fusion in multiagent systems is introduced. Agents individual perceptual capabilities are represented by similarity relations, further aggregated to express joint capabilities of teams, This aggregation, expressing a shift from individual to social level of agents activity, has been formalized by means of dynamic logic. The approach of Doherty et al. (2007) [6] uses the full propositional dynamic logic, which does not guarantee tractability of reasoning. Our idea is to adapt the techniques of Nguyen [2628] to provide an engine for tractable approximate database querying restricted to a Horn fragment of serial dynamic logic. We also show that the obtained formalism is quite powerful in applications. 
.

2009  
[32] 
2009. Annotation Theories over Finite Graphs. Studia Logica: An International Journal for Symbolic Logic, 93(23):147–180. Springer. DOI: 10.1007/s1122500992203. In the current paper we consider theories with vocabulary containing a number of binary and unary relation symbols. Binary relation symbols represent labeled edges of a graph and unary relations represent unique annotations of the graph’s nodes. Such theories, which we call <em>annotation theories</em>, can be used in many applications, including the formalization of argumentation, approximate reasoning, semantics of logic programs, graph coloring, etc. We address a number of problems related to annotation theories over finite models, including satisfiability, querying problem, specification of preferred models and model checking problem. We show that most of considered problems are NPTime or coNPTimecomplete. In order to reduce the complexity for particular theories, we use secondorder quantifier elimination. To our best knowledge none of existing methods works in the case of annotation theories. We then provide a new secondorder quantifier elimination method for stratified theories, which is successful in the considered cases. The new result subsumes many other results, including those of [2, 28, 21]. 
.

[31] 
2009. Voting by Eliminating Quantifiers. Studia Logica: An International Journal for Symbolic Logic, 92(3):365–379. Springer. DOI: 10.1007/s1122500992007. Mathematical theory of voting and social choice has attracted much attention. In the general setting one can view social choice as a method of aggregating individual, often conflicting preferences and making a choice that is the best compromise. How preferences are expressed and what is the “best compromise” varies and heavily depends on a particular situation. The method we propose in this paper depends on expressing individual preferences of voters and specifying properties of the resulting ranking by means of firstorder formulas. Then, as a technical tool, we use methods of secondorder quantifier elimination to analyze and compute results of voting. We show how to specify voting, how to compute resulting rankings and how to verify voting protocols. 
.

2008  
[30] 
2008. Towards Incorporating Background Theories into Quantifier Elimination. Journal of applied nonclassical logics, 18(23):325–340. Éditions HermèsLavoisier. DOI: 10.3166/jancl.18.325340. In the paper we present a technique for eliminating quantifiers of arbitrary order, in particular of firstorder. Such a uniform treatment of the elimination problem has been problematic up to now, since techniques for eliminating firstorder quantifiers do not scale up to higherorder contexts and those for eliminating higherorder quantifiers are usually based on a form of monotonicity w.r.t implication (set inclusion) and are not applicable to the firstorder case. We make a shift to arbitrary relations \"ordering\" the underlying universe. This allows us to incorporate background theories into higherorder quantifier elimination methods which, up to now, has not been achieved. The technique we propose subsumes many other results, including the Ackermann's lemma and various forms of fixpoint approaches when the \"ordering\" relations are interpreted as implication and reveals the common principle behind these approaches. 
.

2007  
[29] 
2007. Communication between agents with heterogeneous perceptual capabilities. In real world applications robots and software agents often have to be equipped with higher level cognitive functions that enable them to reason, act and perceive in changing, incompletely known and unpredictable environments. One of the major tasks in such circumstances is to fuse information from various data sources. There are many levels of information fusion, ranging from the fusing of low level sensor signals to the fusing of high level, complex knowledge structures. In a dynamically changing environment even a single agent may have varying abilities to perceive its environment which are dependent on particular conditions. The situation becomes even more complex when different agents have different perceptual capabilities and need to communicate with each other. In this paper, we propose a framework that provides agents with the ability to fuse both low and high level approximate knowledge in the context of dynamically changing environments while taking account of heterogeneous and contextually limited perceptual capabilities. To model limitations on an agent's perceptual capabilities we introduce the idea of partial tolerance spaces. We assume that each agent has one or more approximate databases where approximate relations are represented using lower and upper approximations on sets. Approximate relations are generalizations of rough sets. It is shown how sensory and other limitations can be taken into account when constructing and querying approximate databases for each respective agent. Complex relations inherit the approximativeness of primitive relations used in their definitions. Agents then query these databases and receive answers through the filters of their perceptual limitations as represented by (partial) tolerance spaces and approximate queries. The techniques used are all tractable. © 2005 Elsevier B.V. All rights reserved. 
.

[28] 
2007. Secondorder quantifier elimination in higherorder contexts with applications to the semantical analysis of conditionals. Studia Logica: An International Journal for Symbolic Logic, 87(1):37–50. Springer. DOI: 10.1007/s1122500790754. Secondorder quantifier elimination in the context of classical logic emerged as a powerful technique in many applications, including the correspondence theory, relational databases, deductive and knowledge databases, knowledge representation, commonsense reasoning and approximate reasoning. In the current paper we first generalize the result of Nonnengart and Szalas [17] by allowing secondorder variables to appear within higherorder contexts. Then we focus on a semantical analysis of conditionals, using the introduced technique and Gabbay's semantics provided in [10] and substantially using a thirdorder accessibility relation. The analysis is done via finding correspondences between axioms involving conditionals and properties of the underlying thirdorder relation. © 2007 Springer Science+Business Media B.V. 
.

[27] 
2007. A correspondence framework between threevalued logics and similaritybased approximate reasoning. Fundamenta Informaticae, 75(14):179–193. IOS Press. This paper focuses on approximate reasoning based on the use of similarity spaces. Similarity spaces and the approximated relations induced by them are a generalization of the rough setbased approximations of Pawlak [17, 18]. Similarity spaces are used to define neighborhoods around individuals and these in turn are used to define approximate sets and relations. In any of the approaches, one would like to embed such relations in an appropriate logic which can be used as a reasoning engine for specific applications with specific constraints. We propose a framework which permits a formal study of the relationship between approximate relations, similarity spaces and threevalued logics. Using ideas from correspondence theory for modal logics and constraints on an accessibility relation, we develop an analogous framework for threevalued logics and constraints on similarity relations. In this manner, we can provide a tool which helps in determining the proper threevalued logical reasoning engine to use for different classes of approximate relations generated via specific types of similarity spaces. Additionally, by choosing a threevalued logic first, the framework determines what constraints would be required on a similarity relation and the approximate relations induced by it. Such information would guide the generation of approximate relations for specific applications. 
.

2006  
[26] 
2006. Secondorder Reasoning in Description Logics. Journal of applied nonclassical logics, 16(3  4):517–530. Éditions HermèsLavoisier. DOI: 10.3166/jancl.16.517530. Description logics refer to a family of formalisms concentrated around concepts, roles and individuals. They belong to the most frequently used knowledge representation formalisms and provide a logical basis to a variety of well known paradigms. The main reasoning tasks considered in the area of description logics are those reducible to subsumption. On the other hand, any knowledge representation system should be equipped with a more advanced reasoning machinery. Therefore in the current paper we make a step towards integrating description logics with secondorder reasoning. One of the important motivations behind introducing secondorder formalism follows from the fact that many forms of commonsense and nonmonotonic reasoning used in AI can be modelled within the secondorder logic. To achieve our goal we first extend description logics with a possibility to quantify over concepts. Since one of the main criticisms against the use of secondorder formalisms is their complexity, we next propose secondorder quantifier elimination techniques applicable to a large class of description logic formulas. Finally we show applications of the techniques, in particular in reasoning with circumscribed concepts and approximated terminological formulas. 
.

[25] 
2006. Approximate Databases: A support tool for approximate reasoning. Journal of applied nonclassical logics, 16(12):87–118. Éditions HermèsLavoisier. DOI: 10.3166/jancl.16.87117. Note: Special issue on implementation of logics This paper describes an experimental platform for approximate knowledge databases called the Approximate Knowledge Database (AKDB), based on a semantics inspired by rough sets. The implementation is based upon the use of a standard SQL database to store logical facts, augmented with several query interface layers implemented in JAVA through which extensional, intensional and local closed world nonmonotonic queries in the form of crisp or approximate logical formulas can be evaluated tractably. A graphical database design user interface is also provided which simplifies the design of databases, the entering of data and the construction of queries. The theory and semantics for AKDBs is presented in addition to application examples and details concerning the database implementation. 
.

2003  
[24] 
2003. Preface. Fundamenta Informaticae, 57(24):i–iii. IOS Press. 
.

[23] 
2003. Towards a framework for approximate ontologies. Fundamenta Informaticae, 57(24):147–165. IOS Press. Currently, there is a great deal of interest in developing tools for the generation and use of ontologies on the WWW. These knowledge structures are considered essential to the success of the semantic web, the next phase in the evolution of the WWW. Much recent work with ontologies assumes that the concepts used as building blocks are crisp as opposed to approximate. It is a premise of this paper that approximate concepts and ontologies will become increasingly more important as the semantic web becomes a reality. We propose a framework for specifying, generating and using approximate ontologies. More specifically, (1) a formal framework for defining approximate concepts, ontologies and operations on approximate concepts and ontologies is presented. The framework is based on intuitions from rough set theory, (2) algorithms for automatically generating approximate ontologies from traditional crisp ontologies or from large data sets together with additional knowledge are presented. The knowledge will generally be related to similarity measurements between individual objects in the data sets, or constraints of a logical nature which rule out particular constellations of concepts and dependencies in generated ontologies. The techniques for generating approximate ontologies are parameterizable. The paper provides specific instantiations and examples. 
.

1999  
[22] 
1999. Metaqueries on deductive databases. We introduce the notion of a metaquery on relational databases and a technique which can be used to represent and solve a number of interesting problems from the area of knowledge representation using logic. The technique is based on the use of quantifier elimination and may also be used to query relational databases using a declarative query language called SHQL (SemiHorn Query Language), introduced in [6]. SHQL is a fragment of classical firstorder predicate logic and allows us to define a query without supplying its explicit definition. All SHQL queries to the database can be processed in polynomial time (both on the size of the input query and the size of the database). We demonstrate the use of the technique in problem solving by structuring logical puzzles from the Knights and Knaves domain as SHQL metaqueries on relational databases. We also provide additional examples demonstrating the flexibility of the technique. We conclude with a description of a newly developed software tool, The Logic Engineer, which aids in the description of algorithms using transformation and reduction techniques such as those applied in the metaquerying approach. 
.

[21] 
1999. Declarative PTIME queries for relational databases using quantifier elimination. Journal of logic and computation (Print), 9(5):737–758. Oxford University Press. DOI: 10.1093/logcom/9.5.737. In this paper, we consider the problem of expressing and computing queries on relational deductive databases in a purely declarative query language, called SHQL (SemiHorn Query Language). Assuming the relational databases in question are ordered, we show that all SHQL queries are computable in PTIME (polynomial time) and the whole class of PTIME queries is expressible in SHQL. Although similar results have been proven for fixpoint languages and extensions to datalog, the claim is that SHQL has the advantage of being purely declarative, where the negation operator is interpreted as classical negation, mixed quantifiers may be used and a query is simply a restricted firstorder theory not limited by the rulebased syntactic restrictions associated with logic programs in general. We describe the PTIME algorithm used to compute queries in SHQL which is based in part on quantifier elimination techniques and also consider extending the method to incomplete relational databases using intuitions related to circumscription techniques. 
.

1998  
[20] 
1998. General domain circumscription and its effective reductions. We first define general domain circumscription (GDC) and provide it with a semantics. GDC subsumes existing domain circumscription proposals in that it allows varying of arbitrary predicates, functions, or constants, to maximize the minimization of the domain of a theory. We then show that for the class of semiuniversal theories without function symbols, that the domain circumscription of such theories can be constructively reduced to logically equivalent firstorder theories by using an extension of the DLS algorithm, previously proposed by the authors for reducing secondorder formulas. We also show that for a certain class of domain circumscribed theories, that any arbitrary secondorder circumscription policy applied to these theories is guaranteed to be reducible to a logically equivalent firstorder theory. In the case of semiuniversal theories with functions and arbitrary theories which are not separated, we provide additional results, which although not guaranteed to provide reductions in all cases, do provide reductions in some cases. These results are based on the use of fixpoint reductions. 
.

1997  
[19] 
1997. Computing circumscription revisited: A reduction algorithm. Journal of automated reasoning, 18(3):297–336. Kluwer Academic Publishers. DOI: 10.1023/A:1005722130532. In recent years, a great deal of attention has been devoted to logics of commonsense reasoning. Among the candidates proposed, circumscription has been perceived as an elegant mathematical technique for modeling nonmonotonic reasoning, but difficult to apply in practice. The major reason for this is the secondorder nature of circumscription axioms and the difficulty in finding proper substitutions of predicate expressions for predicate variables. One solution to this problem is to compile, where possible, secondorder formulas into equivalent firstorder formulas. Although some progress has been made using this approach, the results are not as strong as one might desire and they are isolated in nature. In this article, we provide a general method that can be used in an algorithmic manner to reduce certain circumscription axioms to firstorder formulas. The algorithm takes as input an arbitrary secondorder formula and either returns as output an equivalent firstorder formula, or terminates with failure. The class of secondorder formulas, and analogously the class of circumscriptive theories that can be reduced, provably subsumes those covered by existing results. We demonstrate the generality of the algorithm using circumscriptive theories with mixed quantifiers (some involving Skolemization), variable constants, nonseparated formulas, and formulas with nary predicate variables. In addition, we analyze the strength of the algorithm, compare it with existing approaches, and provide formal subsumption results. 
.

1996  
[18] 
1996. On Natural Deduction in FirstOrder Fixpoint Logics. In the current paper we present a powerful technique of obtaining natural deduction proof systems for firstorder fixpoint logics. The term fixpoint logics refers collectively to a class of logics consisting of modal logics with modalities definable at metalevel by fixpoint equations on formulas. The class was found very interesting as it contains most logics of programs with e.g. dynamic logic, temporal logic and the ¯calculus among them. In this paper we present a technique that allows us to derive automatically natural deduction systems for modal logics from fixpoint equations defining the modalities 
.

[17] 
1996. A reduction result for circumscribed semihorn formulas. Circumscription has been perceived as an elegant mathematical technique for modeling nonmonotonic and commonsense reasoning, but difficult to apply in practice due to the use of secondorder formulas. One proposal for dealing with the computational problems is to identify classes of firstorder formulas whose circumscription can be shown to be equivalent to a firstorder formula. In previous work, we presented an algorithm which reduces certain classes of secondorder circumscription axioms to logically equivalent firstorder formulas. The basis for the algorithm is an elimination lemma due to Ackermann. In this paper, we capitalize on the use of a generalization of Ackermann's Lemma in order to deal with a subclass of universal formulas called <em>semiHorn formulas</em>. Our results subsume previous results by Kolaitis and Papadimitriou regarding a characterization of circumscribed definite logic programs which are firstorder expressible. The method for distinguishing which formulas are reducible is based on a boundedness criterion. The approach we use is to first reduce a circumscribed semiHorn formula to a fixpoint formula which is reducible if the formula is bounded, otherwise not. In addition to a number of other extensions, we also present a fixpoint calculus which is shown to be sound and complete for bounded fixpoint formulas. 
.

1994  
[16] 
1994. On an Automated Translation of Modal Proof Rules into Formulas of the Classical Logic. Journal of Applied NonClassical Logics, 4(2):119–127. Éditions HermèsLavoisier. In this paper we study correspondences between modal proof rules and the classical logic. The method we apply is based on an Ackermann's technique of eliminating secondorder quantifiers from formulas. We show that the process of finding suitable correspondences can be reduced to a few simple steps. Moreover, the whole technique can be fully mechanized. We thus provide the reader with a powerful tool, useful in automated translations between modal logics and the classical logic. 
.

1993  
[15] 
1993. On the Correspondence between Modal and Classical Logic: An Automated Approach. Journal of logic and computation (Print), 3(6):605–620. Oxford University Press. DOI: 10.1093/logcom/3.6.605. The current paper is devoted to automated techniques in the correspondence theory. The theory we deal with concerns the problem of finding classical firstorder axioms corresponding to propositional modal schemas. Given a modal schema and a semantics base method of translating propositional modal formulae into classical firstorder ones, we try to derive automatically classica firstorder formulae characterizing precisely the class of frames validating the schema. The technique we consider can, in many cases, be easily applied even without computer support. Although we mainly concentrate on Kripke semantics, the technique we apply is much more general, as it is based on elimination of secondorder quantifiers from formulae. We show many examples of application of the method. These can also serve as new, automated proofs of considered correspondences. 
.

1992  
[14] 
1992. Axiomatizing Fixpoint Logics. 
.

1991  
[13] 
1991. On Strictly Arithmetical Completeness in Logics of Programs. We introduce and discuss a notion of strictly arithmetical completeness related to relative completeness of Cook (1978) and arithmetical completeness of Harel (1978). We present a powerful technique of obtaining strictly arithmetical axiomatizations of logics of programs. Given a modeltheoretic semantics of a logic and a set of formulae defining (in a metalanguage) its nonclassical connectives, we automatically derive strictly arithmetically complete and sound proof systems for this logic. As examples of application of the technique we obtain new axiomatizations of algorithmic logic, (concurrent) dynamic logic and temporal logic. 
.

1989  
[12] 
1989. On Temporal Logic for Distributed Systems and its Application to Processes Communicating by Interrupts. Fundamenta Informaticae, 12(2):191–204. IOS Press. 
.

1988  
[11] 
1988. Towards the Temporal Approach to Abstract Data Types. Fundamenta Informaticae, 11(1):49–64. IOS Press. 
.

[10] 
1988. An Incompleteness Result in Process Algebra. 
.

[9] 
1988. Propositional Description of Finite CauseEffect Structures. An alternative method of describing semantics of causeeffect structures is presented. It is based on a model of discrete dynamic systems. The model is similar to a conditionevent Petri net, differing in the way restrictions on the alterability of actions are imposed. 
.

[8] 
1988. Incompleteness of FirstOrder Temporal Logic with Until. The results presented in this paper concern the axiomatizability problem of firstorder temporal logic with linear and discrete time. We show that the logic is incomplete, i.e., it cannot be provided with a finitistic and complete proof system. We show two incompleteness theorems. Although the first one is weaker (it assumes some firstorder signature), we decided to present it, for its proof is much simpler and contains an interesting fact that finite sets are characterizable by means of temporal formulas. The second theorem shows that the logic is incomplete independently of any particular signature. 
.

1987  
[7] 
1987. A Complete Axiomatic Characterization of FirstOrder Temporal Logic of Linear Time. As shown in (Szalas, 1986, 1986, 1987) there is no finitistic and complete axiomatization of FirstOrder Temporal Logic of linear and discrete time. In this paper we give an infinitary proof system for the logic. We prove that the proof system is sound and complete. We also show that any syntactically consistent temporal theory has a model. As a corollary we obtain that the Downward Theorem of Skolem, Lowenheim and Tarski holds in the case of considered logic. 
.

[6] 
1987. Arithmetical Axiomatization of FirstOrder Temporal Logic. 
.

1986  
[5] 
1986. Concerning the Semantic Consequence Relation in FirstOrder Temporal Logic. In this paper we consider the firstorder temporal logic with linear and discrete time. We prove that the set of tautologies of this logic is not arithmetical (i.e., it is neither <em>Σ</em><sup>0</sup><sub><em>n</em></sub> nor <em>Π</em><sup>0</sup><sub><em>n</em></sub> for any natural number <em>n</em>). Thus we show that there is no finitistic and complete axiomatization of the considered logic. 
.

1985  
[4] 
1985. A Note on PCI: Distributed Processes Communicating by Interrupts. 
.

[3] 
1985. Exception Handling in Parallel Computations. 
.

1984  
[2] 
1984. On an Application of Algorithmic Theory of Stacks. Fundamenta Informaticae, 7(3):378–388. IOS Press. 
.

1981  
[1] 
1981. Algorithmic Logic with Recursive Functions. Fundamenta Informaticae, 4(4):975–995. IOS Press. 
.