Hide abstracts BibTeX entries  
2015  
[129] 
2015. Editorial Material: Towards richer rule languages with polynomial data complexity for the Semantic Web in DATA and KNOWLEDGE ENGINEERING, vol 9697, issue , pp 5777. 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. 
.

[128] 
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. 
.

[127] 
2015. Stability, Supportedness, Minimality and Kleene Answer Set Programs. In Thomas Eiter, Hannes Strass, Mirosław Truszczynski, Stefan Woltran, editors, Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation: Essays Dedicated to Gerhard Brewka on the Occasion of His 60th Birthday, pages 125–140. In series: Lecture Notes in Computer Science #9060. Springer. ISBN: 9783319147253 (softcover), 9783319147260 (eBook). DOI: 10.1007/9783319147260_9. Link to full text: http://www.ida.liu.se/divisions/aiics/pu... Answer Set Programming is a widely known knowledge representation framework based on the logic programming paradigm that has been extensively studied in the past decades. The semantic framework for Answer Set Programs is based on the use of stable model semantics. There are two characteristics intrinsically associated with the construction of stable models for answer set programs. Any member of an answer set is supported through facts and chains of rules and those members are in the answer set only if generated minimally in such a manner. These two characteristics, supportedness and minimality, provide the essence of stable models. Additionally, answer sets are implicitly partial and that partiality provides epistemic overtones to the interpretation of disjunctiver ules and default negation. This paper is intended to shed light on these characteristics by defining a semantic framework for answer set programming based on an extended firstorder Kleene logic with weak and strong negation. Additionally, a definition of strongly supported models is introduced, separate from the minimality assumption explicit in stable models. This is used to both clarify and generate alternative semantic interpretations for answer set programs with disjunctive rules in addition to answer set programs with constraint rules. An algorithm is provided for computing supported models and comparative complexity results between strongly supported and stable model generation are provided. 
.

2014  
[126] 
2014. Tractable Reasoning about Group Beliefs. In ENGINEERING MULTIAGENT SYSTEMS, EMAS 2014, pages 328–350. In series: Lecture Notes in Computer Science #8758. SPRINGER INT PUBLISHING AG. ISBN: 9783319144849, 9783319144832. DOI: 10.1007/9783319144849_17. In contemporary autonomous systems, like robotics, the need to apply group knowledge has been growing consistently with the increasing complexity of applications, especially those involving teamwork. However, classical notions of common knowledge and common belief, as well as their weaker versions, are too complex. Also, when modeling realworld situations, lack of knowledge and inconsistency of information naturally appear. Therefore, we propose a shift in perspective from reasoning in multimodal logics to querying paraconsistent knowledge bases. This opens the possibility for exploring a new approach to group beliefs. To demonstrate expressiveness of our approach, examples of social procedures leading to complex belief structures are constructed via the use of epistemic profiles. To achieve tractability without compromising the expressiveness, as an implementation tool we choose 4QL, a fourvalued rulebased query language. This permits both to tame inconsistency in individual and group beliefs and to execute the social procedures in polynomial time. Therefore, a marked improvement in efficiency has been achieved over systems such as (dynamic) epistemic logics with common knowledge and ATL, for which problems like model checking and satisfiability are PSPACE or even EXPTIMEhard. 
.

[125] 
2014. The web ontology rule language OWL 2 RL+ and its extensions. In Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen, editors, Transactions on Computational Collective Intelligence XIII, pages 152–175. In series: Lecture Notes in Computer Science #8342. Springer Verlag (Germany). ISBN: 9783642544545. DOI: 10.1007/97836425445527. It is known that the OWL 2RL Web Ontology Language Profile has PTime data complexity and can be translated into Datalog. However, the result of translation may consist of a Datalog program and a set of constraints in the form of negative clauses. Therefore, a knowledge base in OWL 2RL may be unsatisfiable. In the current paper we first identify a maximal fragment of OWL 2RL, called OWL 2RL+, with the property that every knowledge base expressed in OWL2RL+ can be translated to a Datalog program and hence is satisfiable. We then propose some extensions of OWL 2RL and OWL 2RL + that still have PTime data complexity. © 2014 SpringerVerlag Berlin Heidelberg. 
.

[124] 
2014. Symbolic Explanations of Generalized Fuzzy Reasoning. In SMART DIGITAL FUTURES 2014, pages 7–16. In series: Frontiers in Artificial Intelligence and Applications #??. IOS Press. ISBN: 9781614994053; 9781614994046. DOI: 10.3233/97816149940537. Various generalizations of fuzzy reasoning are frequently used in decision making. While in many application areas it is natural to assume that truth degrees of a property and its complement sum up to 1, such an assumption appears problematic, e.g., in modeling ignorance. Therefore, in some generalizations of fuzzy sets, degrees of membership in a set and in its complement are separated and are no longer required to sum up to 1. In frequent cases, this separation of positive and negative evidences for concept membership is more natural. As we discuss in the current paper, symbolic explanations of results of such forms of reasoning provide additional important information. In the present paper we address two related questions: (i) given generalized fuzzy connectives and a finite set of truth values T, find a finitelyvalued logic over T, explaining fuzzy reasoning, and (ii) given a finitelyvalued logic, find a fuzzy semantics, explained by the given logic. We also show examples illustrating usefulness of the approach. 
.

[123] 
2014. On horn knowledge bases in regular description logic with inverse. In KNOWLEDGE AND SYSTEMS ENGINEERING (KSE 2013), VOL 1, pages 37–49. In series: Advances in Intelligent Systems and Computing #Vol 244. Springer Berlin/Heidelberg. ISBN: 9783319027401. DOI: 10.1007/9783319027418_6. 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 fragmentsEL, DLLite, DLP, HornSH IQ and HornSROIQof 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. 
.

[122] 
2014. WORL: a nonmonotonic rule language for the semantic web. Vietnam Journal of Computer Science, 1(1):57–69. Springer Berlin/Heidelberg. DOI: 10.1007/s405950130009y. 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  
[121] 
2013. HornDL: An Expressive Horn Description Logic with PTime Data Complexity. In Wolfgang Faber, Domenico Lembo, editors, Web Reasoning and Rule Systems, pages 259–264. In series: Lecture Notes in Computer Science #7994. Springer Berlin/Heidelberg. ISBN: 9783642396656 (print), 9783642396663 (online). DOI: 10.1007/9783642396663_25. We introduce a Horn description logic called HornDL, which is strictly and essentially richer than Horn SROIQ , while still has PTime data complexity. In comparison with Horn SROIQ , HornDL additionally allows the universal role and assertions of the form irreflexive <em>(s)</em>, ¬s(a,b) , a≐̸b . More importantly, in contrast to all the wellknown Horn fragments EL , DLLite, DLP, Horn SHIQ , Horn SROIQ 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. In the long version of this paper, we present the first algorithm with PTime data complexity for checking satisfiability of HornDL knowledge bases. 
.

[120] 
2013. HornTeamLog: A Horn Fragment of TeamLog with PTime Data Complexity. In Costin Bǎdicǎ, Ngoc Thanh Nguyen, Marius Brezovan, editors, Computational Collective Intelligence. Technologies and Applications, pages 143–153. In series: Lecture Notes in Computer Science #8083. Springer Berlin/Heidelberg. ISBN: 9783642404948 (print), 9783642404955 (online). DOI: 10.1007/9783642404955_15. The logic TeamLog proposed by DuninKęplicz and Verbrugge is used to express properties of agents’ cooperation in terms of individual, bilateral and collective informational and motivational attitudes like beliefs, goals and intentions. In this paper we isolate a Horn fragment of TeamLog, called HornTeamLog, and we show that it has PTime data complexity. 
.

[119] 
2013. On the Horn Fragments of Serial Regular Grammar Logics with Converse. In Dariusz Barbucha, Manh Thanh Le, Robert J. Howlett, Lakhmi C. Jain, editors, Advanced Methods and Technologies for Agent and MultiAgent Systems: Proceedings of the 7th KES Conference on Agent and MultiAgent Systems  Technologies and Applications (KESAMSTA 2013), pages 225–234. In series: Frontiers in Artificial Intelligence and Applications #252. IOS Press. ISBN: 9781614992530. DOI: 10.3233/9781614992547225. We study Horn fragments of serial multimodal logics which are characterized by regular grammars with converse. Such logics are useful for reasoning about epistemic states of multiagent systems as well as similaritybased approximate reasoning. We provide the first algorithm with PTIME data complexity for checking satisfiability of a Horn knowledge base in a serial regular grammar logic with converse. 
.

[118] 
2013. Partiality and Inconsistency in Agents' Belief Bases. In Dariusz Barbucha, Manh Thanh Le, Robert J. Howlett, Lakhmi C. Jain, editors, Advanced Methods and Technologies for Agent and MultiAgent Systems: Proceedings of the 7th KES Conference on Agent and MultiAgent Systems  Technologies and Applications (KESAMSTA 2013), pages 3–17. In series: Frontiers in Artificial Intelligence and Applications #252. IOS Press. ISBN: 9781614992530. DOI: 10.3233/97816149925473. Agents' beliefs can be incomplete and partially inconsistent. The process of agents' belief formation in such contexts has to be supported by suitable tools allowing one to express a variety of inconsistency resolving and nonmonotonic reasoning techniques.In this paper we discuss 4QL*, a general purpose rulebased query language allowing one to use rules with negation in the premises and in the conclusions 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, it is tractable w.r.t. data complexity and captures PTIME queries, so can be used in realworld applications.Reasoning in 4QL* is based on wellsupported models. We simplify and at the same time generalize previous definitions of wellsupported models and develop a new algorithm for computing such models. 
.

[117] 
2013. Perceiving Speech Acts under Incomplete and Inconsistent Information. In Dariusz Barbucha, Manh Thanh Le, Robert J. Howlett, Lakhmi C. Jain, editors, Advanced Methods and Technologies for Agent and MultiAgent Systems: Proceedings of the 7th KES Conference on Agent and MultiAgent Systems  Technologies and Applications (KESAMSTA 2013), pages 255–264. In series: Frontiers in Artificial Intelligence and Applications #252. IOS Press. ISBN: 9781614992530. DOI: 10.3233/9781614992547255. 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, DATALOG$^{\neg \neg}$like query language 4QL as a fourvalued implementation framework ensures that, in contrast to the standard twovalued approaches, tractability of the model is achieved. 
.

[116] 
2013. Taming Complex Beliefs. In Ngoc Thanh Nguyen, editor, Transactions on Computational Collective Intelligence XI, pages 1–21. In series: Lecture Notes in Computer Science #8065. Springer Berlin/Heidelberg. ISBN: 9783642417757 (print), 9783642417764 (online). DOI: 10.1007/9783642417764_1. A novel formalization of beliefs in multiagent systems has recently been proposed by DuninKęplicz and Szałas. The aim has been to bridge the gap between idealized logical approaches to modeling beliefs and their actual implementations. Therefore the stages of belief acquisition, intermediate reasoning and final belief formation have been isolated and analyzed. In conclusion, a novel semantics reflecting those stages has been provided. This semantics is based on the new concept of epistemic profile, reflecting agent’s reasoning capabilities in a dynamic and unpredictable environment. The presented approach appears suitable for building complex belief structures in the context of incomplete and/or inconsistent information. One of original ideas is that of epistemic profiles serving as a tool for transforming preliminary beliefs into final ones. As epistemic profile can be devised both on an individual and a group level in analogical manner, a uniform treatment of single agent and group beliefs has been achieved.In the current paper these concepts are further elaborated. Importantly, we indicate an implementation framework ensuring tractability of reasoning about beliefs, propose the underlying methodology and illustrate it on an example. 
.

[115] 
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>. 
.

[114] 
2013. LogicBased Roughification. In Andrzej Skowron, Zbigniew Suraj, editors, Rough Sets and Intelligent Systems  Professor Zdzisław Pawlak in Memoriam (vol. I), pages 517–543. In series: Intelligent Systems Reference Library #42. Springer Berlin/Heidelberg. ISBN: 9783642303432. DOI: 10.1007/9783642303449_19. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/13601690 find book in another country/hitta boken i ett annat land: http://www.worldcat.org/title/roughsets... This book is dedicated to the memory of Professor Zdzis{\l}aw Pawlak who passed away almost six year ago. He is the founder of the Polish school of Artificial Intelligence and one of the pioneers in Computer Engineering and Computer Science with worldwide influence. He was a truly great scientist, researcher, teacher and a human being.This book prepared in two volumes contains more than 50 chapters. This demonstrates that the scientific approaches discovered by of Professor Zdzis{\l}aw Pawlak, especially the rough set approach as a tool for dealing with imperfect knowledge, are vivid and intensively explored by many researchers in many places throughout the world. The submitted papers prove that interest in rough set research is growing and is possible to see many new excellent results both on theoretical foundations and applications of rough sets alone or in combination with other approaches.We are proud to offer the readers this book. 
.

[113] 
2013. Distributed Paraconsistent Belief Fusion. In Giancarlo Fortino , Costin Badica , Michele Malgeri and Rainer Unland, editors, Intelligent Distributed Computing VI: Proceedings of the 6th International Symposium on Intelligent Distributed Computing  IDC 2012, Calabria, Italy, September 2012, pages 59–69. In series: Studies in Computational Intelligence #446. Springer Berlin/Heidelberg. ISBN: 9783642325236 (print), 9783642325243 (online). DOI: 10.1007/9783642325243_9. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/13601893 The current paper is devoted to belief fusion when information sources may deliver incomplete and inconsistent information. In such cases paraconsistent and commonsense reasoning techniques can be used to complete missing knowledge and disambiguate inconsistencies. We propose a novel, realistic model of distributed belief fusion and an implementation framework guaranteeing its tractability. 
.

2012  
[112] 
2012. Concept Learning for Description Logicbased Information Systems. In KSE 2012  International Conference on Knowledge and Systems Engineering, pages 65–73. IEEE Computer Society. DOI: 10.1109/KSE.2012.23. 
.

[111] 
2012. A Bisimulationbased Method of Concept Learning for Knowledge Bases in Description Logics. In SoICT 2012  3rd International Symposium on Information and Communication Technology, pages 241–249. ACM Press. DOI: 10.1145/2350716.2350753. We develop the first bisimulationbased method of concept learning, called BBCL, for knowledge bases in description logics (DLs). Our method is formulated for a large class of useful DLs, with wellknown DLs like <em>ALC, SHIQ, SHOIQ, SROIQ</em>. As bisimulation is the notion for characterizing indiscernibility of objects in DLs, our method is natural and very promising. 
.

[110] 
2012. Epistemic Profiles and Belief Structures. In Gordan Jezic, Mario Kusek, NgocThanh Nguyen, Robert J. Howlett, Lakhmi C. Jain, editors, Agent and MultiAgent Systems. Technologies and Applications: 6th KES International Conference, KESAMSTA 2012, Dubrovnik, Croatia, June 2527, 2012. Proceedings, pages 360–369. In series: Lecture Notes in Computer Science #7327. Springer Berlin/Heidelberg. ISBN: 9783642309465, e 9783642309472. DOI: 10.1007/9783642309472_40. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/13481324 find book in another country/hitta boken i ett annat land: http://www.worldcat.org/search?q=Agent+a... This book constitutes the refereed proceedings of the 6th KES International Conference on Agent and MultiAgent Systems, KESAMSTA 2012, held in Dubrovnik, Croatia, in June 2012. <br>The conference attracted a substantial number of researchers and practitioners from all over the world who submitted their papers for ten main tracks covering the methodology and applications of agent and multiagent systems, one workshop (TRUMAS 2012) and five special sessions on specific topics within the field. The 66 revised papers presented were carefully reviewed and selected for inclusion in the book. The papers are organized in topical sections on virtual organizations, knowledge and learning agents, intelligent workflow, cloud computing and intelligent systems, selforganization, ICTbased alternative and augmentative communication, multiagent systems, mental and holonic models, assessment methodologies in multiagent and other paradigms, business processing agents, Trumas 2012 (first international workshop), conversational agents and agent teams, digital economy, and multiagent systems in distributed environments. 
.

[109] 
2012. Paraconsistent Reasoning for Semantic Web Agents. In Ngoc Thanh Nguyen, editor, Transactions on Computational Collective Intelligence VI, pages 36–55. In series: Lecture Notes in Computer Science #7190. Springer Berlin/Heidelberg. ISBN: 9783642293559, 9783642293566. DOI: 10.1007/9783642293566_2. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/13481193 find book in another country/hitta boken i ett annat land: http://www.worldcat.org/search?q=Transac... The LNCS journal Transactions on Computational Collective Intelligence (TCCI) focuses on all facets of computational collective intelligence (CCI) and their applications in a wide range of fields such as the Semantic Web, social networks and multiagent systems. TCCI strives to cover new methodological, theoretical and practical aspects of CCI understood as the form of intelligence that emerges from the collaboration and competition of many individuals (artificial and/or natural). The application of multiple computational intelligence technologies such as fuzzy systems, evolutionary computation, neural systems, consensus theory, etc., aims to support human and other collective intelligence and to create new forms of CCI in natural and/or artificial systems.This, the sixth issue of Transactions on Computational Collective Intelligence contains 10 selected papers, focusing on the topics of classification, agent cooperation, paraconsistent reasoning and agent distributed mobile interaction. 
.

[108] 
2012. Agents in Approximate Environments. In Jan Ejick and Rineke Verbrugge, editors, Games, Actions and Social Software: Multidisciplinary Aspects, pages 141–163. In series: Lecture Notes in Computer Science #7010. Springer. ISBN: 9783642293252 (print), 9783642293269 (online). DOI: 10.1007/9783642293269_8. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/13428777 find book in another country/hitta boken i ett annat land: http://www.worldcat.org/search?q=Games%2... Edited in collaboration with FoLLI, the Association of Logic, Language and Information, this book collects a set of chapters of the multidisciplinary project \"Games, actions and Social software\" which was carried out at the Netherlands Institute for Advanced Study in the Humanities and Social Sciences (NIAS) in Wassenaar, from September 2006 through January 2007.<br>The chapters focus on social software and the social sciences, knowledge, belief and action, perception, communication, and cooperation. 
.

[107] 
2012. Temporal Composite Actions with Constraints. In Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 478–488. AAAI Press. ISBN: 9781577355601, 9781577355618. Link: http://www.aaai.org/ocs/index.php/KR/KR1... Complex mission or task specification languages play a fundamentally important role in human/robotic interaction. In realistic scenarios such as emergency response, specifying temporal, resource and other constraints on a mission is an essential component due to the dynamic and contingent nature of the operational environments. It is also desirable that in addition to having a formal semantics, the language should be sufficiently expressive, pragmatic and abstract. The main goal of this paper is to propose a mission specification language that meets these requirements. It is based on extending both the syntax and semantics of a wellestablished formalism for reasoning about action and change, Temporal Action Logic (TAL), in order to represent temporal composite actions with constraints. Fixpoints are required to specify loops and recursion in the extended language. The results include a sound and complete proof theory for this extension. To ensure that the composite language constructs are adequately grounded in the pragmatic operation of robotic systems, Task Specification Trees (TSTs) and their mapping to these constructs are proposed. The expressive and pragmatic adequacy of this approach is demonstrated using an emergency response scenario. 
.

2011  
[106] 
2011. Living with Inconsistency and Taming Nonmonotonicity. In O. de Moor, G. Gottlob, T. Furche, A. Sellers, editors, Datalog Reloaded, pages 334–398. In series: Lecture Notes in Computer Science #6702. Springer Berlin/Heidelberg. ISBN: 9783642242052. DOI: 10.1007/9783642242069_22. In this paper we consider rulebased query languages with negation inbodies and heads of rules, traditionally denoted by DATALOG. Tractable andat the same time intuitive semantics for DATALOG has not been provided evenif the area of deductive databases is over 30 years old. In this paper we identifysources of the problem and propose a query language, which we call 4QL.The 4QL language supports a modular and layered architecture and providesa tractable framework for many forms of rulebased reasoning both monotonicand nonmonotonic. As the underpinning principle we assume openness of theworld, which may lead to the lack of knowledge. Negation in rule heads may leadto inconsistencies. To reduce the unknown/inconsistent zones we introduce simpleconstructs which provide means for applicationspecific disambiguation ofinconsistent information, the use of Local Closed World Assumption (thus alsoClosed World Assumption, if needed), as well as various forms of default anddefeasible reasoning. 
.

[105] 
2011. WORL: A Web Ontology Rule Language. In Proceedings of the 3rd International Conference on Knowledge and Systems Engineering (KSE), pages 32–39. IEEE. ISBN: 9781457718489. DOI: 10.1109/KSE.2011.14. We develop a Web ontology rule language, called WORL, which combines a variant of OWL 2 RL with eDatalogwithnegation. We disallow the features of OWL 2 RL that play the role of constraints (i.e., the ones that are translated to negative clauses), but allow additional features like negation, the minimal number restriction and unary external checkable predicates to occur in the left hand side of concept inclusion axioms. Some restrictions are adopted to guarantee a translation into eDatalogwithnegation. We also develop the wellfounded semantics for WORL and the standard semantics for stratified WORL (SWORL) via translation into eDatalogwithnegation. Both WORL and SWORL 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. 
.

[104] 
2011. Tractable model checking for fragments of higherorder coalition logic. In Liz Sonenberg, Peter Stone, Kagan Tumer, Pinar Yolum, editors, Proceedings of the 10th International Conference on Autonomous Agents and Multiagent Systems  Volume 2, pages 743–750. AAAI Press. ISBN: 0982657161, 9780982657164. Link: http://dl.acm.org/citation.cfm?id=203172... A number of popular logical formalisms for representing and reasoning about the abilities of teams or coalitions of agents have been proposed beginning with the Coalition Logic (CL) of Pauly. Ågotnes et al introduced a means of succinctly expressing quantification over coalitions without compromising the computational complexity of model checking in CL by introducing Quantified Coalition Logic (QCL). QCL introduces a separate logical language for characterizing coalitions in the modal operators used in QCL. Boella et al, increased the representational expressibility of such formalisms by introducing HigherOrder Coalition Logic (HCL), a monadic secondorder logic with special set grouping operators. Tractable fragments of HCL suitable for efficient model checking have yet to be identified. In this paper, we relax the monadic restriction used in HCL and restrict ourselves to the diamond operator. We show how formulas using the diamond operator are logically equivalent to secondorder formulas. This permits us to isolate and define wellbehaved expressive fragments of secondorder logic amenable to modelchecking in PTime. To do this, we appeal to techniques used in deductive databases and quantifier elimination. In addition, we take advantage of the monotonicity of the effectivity function resulting in exponentially more succinct representation of models. The net result is identification of highly expressible fragments of a generalized HCL where model checking can be done efficiently in PTime. 
.

[103] 
2011. On the Web Ontology Rule Language OWL 2 RL. In Piotr Jedrzejowicz, Ngoc Thanh Nguyen and Kiem Hoang, editors, Proceedings of the 3rd International Conference on Computational Collective Intelligence, Technologies and Applications (ICCCI), pages 254–264. In series: Lecture Notes in Computer Science #6922. Springer Berlin/Heidelberg. ISBN: 9783642239342. DOI: 10.1007/9783642239359_25. It is known that the OWL 2 RL Web Ontology Language Profile has PTime data complexity and can be translated into Datalog. However, a knowledge base in OWL 2 RL may be unsatisfiable. The reason is that, when translated into Datalog, the result may consist of a Datalog program and a set of constraints in the form of negative clauses. In this paper we first identify a maximal fragment of OWL 2 RL called OWL 2 RL<sup> + </sup>with the property that every knowledge base expressed in this fragment can be translated into a Datalog program and hence is satisfiable. We then propose some extensions of OWL 2 RL and OWL 2 RL<sup> + </sup> that still have PTime data complexity. 
.

[102] 
2011. Contextual Coalitional Games. In Mohua Banerjee, Anil Seth, editors, Proceedings of the 4th Indian Conference on Logic and its Applications (ICLA), pages 65–78. In series: Lecture Notes in Artificial Intelligence #6521. Springer Berlin/Heidelberg. DOI: 10.1007/9783642180262_7. The study of cooperation among agents is of central interest in multiagent systems research. A popular way to model cooperation is through coalitional game theory. Much research in this area has had limited practical applicability as regards realworld multiagent systems due to the fact that it assumes<em>deterministic</em> payoffs to coalitions and in addition does not apply to multiagent environments that are<em>stochastic</em> in nature. In this paper, we propose a novel approach to modeling such scenarios where coalitional games will be contextualized through the use of logical expressions representing environmental and other state, and probability distributions will be placed on the space of contexts in order to model the stochastic nature of the scenarios. More formally, we present a formal representation language for representing contextualized coalitional games embedded in stochastic environments and we define and show how to compute <em>expected Shapley values</em> in such games in a computationally efficient manner. We present the value of the approach through an example involving robotics assistance in emergencies. 
.

[101] 
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> 
.

[100] 
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. 
.

[99] 
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  
[98] 
2010. Graded Beliefs, Goals and Intentions. In Proceedings of the 3rd Workshop on Logical Aspects of MultiAgent Systems (LAMAS), pages 1–15. AAAI Press. 
.

[97] 
2010. ThreeValued Paraconsistent Reasoning for Semantic Web Agents. In Proceedings of the 4th International KES Symposium on Agents and Multiagent Systems – Technologies and Applications (KESAMSTA), pages 152–162. In series: Lecture Notes in Artificial Intelligence #6070. Springer. ISBN: 9783642134791. DOI: 10.1007/9783642134807_17. Description logics [1] refer to a family of formalisms concentrated around concepts, roles and individuals. They are used in many multiagent and semantic web applications as a foundation for specifying knowledge bases and reasoning about them. One of widely applied description logics is <em>SHIQ</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\" /><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char49.png\" /><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char51.png\" /> [7,8]. In the current paper we address the problem of inconsistent knowledge. Inconsistencies may naturally appear in the considered application domains, for example as a result of fusing knowledge from distributed sources. We define three threevalued paraconsistent semantics for <em>SHIQ</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\" /><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char49.png\" /><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char51.png\" />, reflecting different meanings of concept inclusion of practical importance. We also provide a quite general syntactic condition of safeness guaranteeing satisfiability of a knowledge base w.r.t. threevalued semantics and define a faithful translation of our formalism into a suitable version of a twovalued description logic. Such a translation allows one to use existing tools and <em>SHIQ</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\" /><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char49.png\" /><img src=\"http://www.springerlink.com/jsMath/fonts/cmsy10/alpha/120/char51.png\" /> reasoners to deal with inconsistent knowledge. 
.

[96] 
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. 
.

[95] 
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. 
.

[94] 
2010. On the Correctness of RoughSet Based Approximate Reasoning. In M. Szczuka, M. Kryszkiewicz, S. Ramanna, R. Jensen, Q. Hu, editors, Proceedings of the 7th International Conference on Rough Sets and Current Trends in Computing (RSCTC), pages 327–336. In series: Lecture Notes in Computer Science #6086. Springer. ISBN: 9783642135286. DOI: 10.1007/9783642135293_35. There is a natural generalization of an indiscernibility relation used in rough set theory, where rather than partitioning the universe of discourse into indiscernibility classes, one can consider a covering of the universe by similaritybased neighborhoods with lower and upper approximations of relations defined via the neighborhoods. When taking this step, there is a need to tune approximate reasoning to the desired accuracy. We provide a framework for analyzing selfadaptive knowledge structures. We focus on studying the interaction between inputs and output concepts in approximate reasoning. The problems we address are: given similarity relations modeling approximate concepts, what are similarity relations for the output concepts that guarantee correctness of reasoning? assuming that output similarity relations lead to concepts which are not accurate enough, how can one tune input similarities? 
.

[93] 
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. 
.

[92] 
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. 
.

[91] 
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  
[90] 
2009. Fusing Approximate Knowledge from Distributed Sources. In Proceedings of the 3rd International Symposium on Intelligent Distributed Computing (IDC), pages 75–86. In series: Studies in Computational Intelligence #237. Springer Berlin/Heidelberg. ISBN: 9783642032134, 9783642269301. DOI: 10.1007/9783642032141_8. In this paper we investigate a technique for fusing approximate knowledge obtained from distributed, heterogeneous information sources. We use a generalization of rough sets and relations [14], which depends on allowing arbitrary similarity relations. The starting point of this research is [2], where a framework for knowledge fusion in multiagent systems is introduced. Agent’s individual perceptual capabilities are represented by similarity relations, further aggregated to express joint capabilities of teams. This aggregation, allowing a shift from individual to social level, has been formalized by means of dynamic logic. The approach of [2] uses the full propositional dynamic logic, not guaranteeing the tractability of reasoning. Therefore the results of [11, 12, 13] are adapted to provide a technical engine for tractable approximate database querying restricted to a Horn fragment of serial PDL. We also show that the obtained formalism is quite powerful in applications. 
.

[89] 
2009. Checking Consistency of an ABox w.r.t. Global Assumptions in PDL*. In Proceedings of the 18th Concurrency, Specification and Programming Workshop (CS&P), pages 431–442. 
.

[88] 
2009. An Optimal Tableau Decision Procedure for ConversePDL. In Proceedings of the 1st International Conference on Knowlegde and Systems Engineering (KSE), pages 207–214. IEEE Computer Society. ISBN: 9781424450862. DOI: 10.1109/KSE.2009.12. We give a novel tableau calculus and an optimal (EXPTIME) tableau decision procedure based on the calculus for the satisfiability problem of propositional dynamic logic with converse. Our decision procedure is formulated with global caching and can be implemented together with useful optimization techniques. 
.

[87] 
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]. 
.

[86] 
2009. Paraconsistent Reasoning with Words. In Aspects of Natural Language Processing: Essays Dedicated to Leonard Bolc on the Occasion of His 75th Birthday, pages 43–58. In series: Lecture Notes in Computer Science #5070. Springer. ISBN: 9783642047343. DOI: 10.1007/9783642047350_2. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/11741557 Fuzzy logics are one of the most frequent approaches to model uncertainty and vagueness. In the case of fuzzy modeling, degrees of belief and disbelief sum up to 1, which causes problems in modeling the lack of knowledge and inconsistency. Therefore, so called paraconsistent intuitionistic fuzzy sets have been introduced, where the degrees of belief and disbelief are not required to sum up to 1. The situation when this sum is smaller than 1 reflects the lack of knowledge and its value greater than 1 models inconsistency. In many applications there is a strong need to guide and interpret fuzzylike reasoning using qualitative approaches. To achieve this goal in the presence of uncertainty, lack of knowledge and inconsistency, we provide a framework for qualitative interpretation of the results of fuzzylike reasoning by labeling numbers with words, like <em>true, false, inconsistent, unknown</em>, reflecting truth values of a suitable, usually finitely valued logical formalism. 
.

[85] 
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. 
.

[84] 
2009. EXPTIME Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic ALC. In Ngoc Thanh; Kowalczyk, Ryszard; Chen, ShyiMing, editors, Proceedings of the 1st International Conference on Computational Collective Intelligence  Semantic Web, Social Networks & Multiagent Systems (ICCCI), pages 437–448. In series: Lecture Notes in Artificial Intelligence #5796. Springer. ISBN: 9783642044403 (print), 9783642044410 (online). DOI: 10.1007/9783642044410_38. We give the first ExpTime (optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic ALC, not based on transformation that encodes ABoxes by nominals or terminology axioms. Our procedure can be implemented as an extension of the highly optimized tableau prover TGC [12] to obtain an efficient program for the mentioned satisfiability problem. 
.

[83] 
2009. A tableau calculus for regular grammar logics with converse. In Proceedings of the 22nd International Conference on Automated Deduction (CADE), pages 421–436. In series: Lecture Notes in Artificial Intelligence #5663. Springer. ISBN: 9783642029585. DOI: 10.1007/9783642029592_31. We give a sound and complete tableau calculus for deciding the general satisfiability problem of regular grammar logics with converse (REG c logics). Tableaux of our calculus are defined as \"andor\" graphs with global caching. Our calculus extends the tableau calculus for regular grammar logics given by Goré and Nguyen [11] by using a cut rule and existential automatonmodal operators to deal with converse. We use it to develop an ExpTime (optimal) tableau decision procedure for the general satisfiability problem of REG c logics. We also briefly discuss optimizations for the procedure. 
.

2008  
[82] 
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. 
.

[81] 
2008. Reasoning with Qualitative Preferences and Cardinalities Using Generalized Circumscription. In Gerhard Brewka, Jérôme Lang, editors, Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 560–570. AAAI Press. ISBN: 9781577353843. The topic of preference modeling has recently attracted the interest of a number of subdisciplines in artificial intelligence such as the nonmonotonic reasoning and action and change communities. The approach in these communities focuses on qualitative preferences and preference models which provide more natural representations from a~commonsense perspective. In this paper, we show how generalized circumscription can be used as a highly expressive framework for qualitative preference modeling. Generalized circumscription proposed by Lifschitz allows for predicates (and thus formulas) to be minimized relative to arbitrary preorders (reflexive and transitive). Although it has received little attention, we show how it may be used to model and reason about elaborate qualitative preference relations. One of the perceived weaknesses with any type of circumscription is the 2ndorder nature of the representation. The paper shows how a large variety of preference theories represented using generalized circumscription can in fact be reduced to logically equivalent firstorder theories in a constructive way. Finally, we also show how preference relations represented using general circumscription can be extended with cardinality constraints and when these extensions can also be reduced to logically equivalent firstorder theories. 
.

[80] 
2008. SecondOrder Quantifier Elimination. Foundations, Computational Aspects and Applications. Book.
In series: Studies in Logics #12. College Publications. 308 pages. ISBN: 9781904987567, 1904987567. link: http://www.amazon.com/SecondOrderQuant... In recent years there has been an increasing use of logical methods and significant new developments have been spawned in several areas of computer science, ranging from artificial intelligence and software engineering to agentbased systems and the semantic web. In the investigation and application of logical methods there is a tension between: * the need for a representational language strong enough to express domain knowledge of a particular application, and the need for a logical formalism general enough to unify several reasoning facilities relevant to the application, on the one hand, and * the need to enable computationally feasible reasoning facilities, on the other hand. Secondorder logics are very expressive and allow us to represent domain knowledge with ease, but there is a high price to pay for the expressiveness. Most secondorder logics are incomplete and highly undecidable. It is the quantifiers which bind relation symbols that make secondorder logics computationally unfriendly. It is therefore desirable to eliminate these secondorder quantifiers, when this is mathematically possible; and often it is. If secondorder quantifiers are eliminable we want to know under which conditions, we want to understand the principles and we want to develop methods for secondorder quantifier elimination. This book provides the first comprehensive, systematic and uniform account of the stateoftheart of secondorder quantifier elimination in classical and nonclassical logics. It covers the foundations, it discusses in detail existing secondorder quantifier elimination methods, and it presents numerous examples of applications and nonstandard uses in different areas. These include: * classical and nonclassical logics, * correspondence and duality theory, * knowledge representation and description logics, * commonsense reasoning and approximate reasoning, * relational and deductive databases, and * complexity theory. The book is intended for anyone interested in the theory and application of logics in computer science and artificial intelligence. 
.

[79] 
2008. Fourvalued Extension of Rough Sets. In Proceedings of the 3rd International Conference Rough Sets and Knowledge Technology (RSKT), pages 106–114. In series: Lecture Notes in Computer Science #5009. Springer. ISBN: 9783540797203. DOI: 10.1007/9783540797210_19. Rough set approximations of Pawlak [15] are sometimes generalized by using similarities between objects rather than elementary sets. In practical applications, both knowledge about properties of objects and knowledge of similarity between objects can be incomplete and inconsistent. The aim of this paper is to define set approximations when all sets, and their approximations, as well as similarity relations are fourvalued. A set is fourvalued in the sense that its membership function can have one of the four logical values: unknown (<strong>u</strong>), false (<strong>f</strong>), inconsistent (<strong>i</strong>), or true (<strong>t</strong>). To this end, a new implication operator and settheoretical operations on fourvalued sets, such as set containment, are introduced. Several properties of lower and upper approximations of fourvalued sets are also presented. 
.

[78] 
2008. Paraconsistent Logic Programs with Fourvalued Rough Sets. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pages 41–51. In series: Lecture Notes in Computer Science #5306. Springer. ISBN: 9783540884231 (print), 9783540884255 (online). DOI: 10.1007/9783540884255_5. This paper presents a language for defining fourvalued rough sets and to reason about them. Our framework brings together two major fields: rough sets and paraconsistent logic programming. On the one hand it provides a paraconsistent approach, based on fourvalued rough sets, for integrating knowledge from different sources and reasoning in the presence of inconsistencies. On the other hand, it also caters for a specific type of uncertainty that originates from the fact that an agent may perceive different objects of the universe as being indiscernible. This paper extends the ideas presented in [9]. Our language allows the user to define similarity relations and use the approximations induced by them in the definition of other fourvalued sets. A positive aspect is that it allows users to tune the level of uncertainty or the source of uncertainty that best suits applications. 
.

2007  
[77] 
2007. Towards Approximate BGI Systems. In Proceedings of the 5th International Central and Eastern European Conference on MultiAgent Systems (CEEMAS), pages 277–287. In series: Lecture Notes in Artificial Intelligence #4696. Springer Berlin/Heidelberg. ISBN: 9783540752530. DOI: 10.1007/9783540752547_28. This paper focuses on modelling perception and vague concepts in the context of multiagent Bgi (<em>Beliefs, Goals</em> and <em>Intentions</em>) systems. The starting point is the multimodal formalization of such systems. Then we make a shift from Kripke structures to similarity structures, allowing us to model perception and vagueness in an uniform way, “compatible” with the multimodal approach. As a result we introduce and discuss <em>approximate B</em> <em>gi</em> <em>systems</em>, which can also be viewed as a way to implement multimodal specifications of Bgi systems in the context of perception. 
.

[76] 
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. 
.

[75] 
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. 
.

[74] 
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. 
.

[73] 
2007. Dynamics of approximate information fusion. In Proceedings of the International Conference on Rough Sets and Emerging Intelligent Systems Paradigms (RSEISP), pages 668–677. In series: Lecture Notes in Artificial Intelligence #4585. Springer Berlin/Heidelberg. ISBN: 9783540734505. DOI: 10.1007/9783540734512_70. The multiagent system paradigm has proven to be a useful means of abstraction when considering distributed systems with interacting components. It is often the case that each component may be viewed as an intelligent agent with specific and often limited perceptual capabilities. It is also the case that these agent components may be used as information sources and such sources may be aggregated to provide global information about particular states, situations or activities in the embedding environment. This paper investigates a framework for information fusion based on the use of generalizations of rough set theory and the use of dynamic logic as a basis for aggregating similarity relations among objects where the similarity relations represent individual agents perceptual capabilities or limitations. As an added benefit, it is shown how this idea may also be integrated into description logics. 
.

[72] 
2007. A FourValued Logic for Rough SetLike Approximate Reasoning. In James F. Peters, Andrzej Skowron, Ivo Düntsch, Jerzy GrzymalaBusse, Ewa Orlowska and Lech Polkowski, editors, Transactions on Rough Sets VI, pages 176–190. In series: Lecture Notes in Computer Science #4374/2007. Springer. ISBN: 3540711988, 9783540711988. DOI: 10.1007/9783540712008_11. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/11381912 Annotation The LNCS journal Transactions on Rough Sets is devoted to the entire spectrum of rough sets related issues, from logical and mathematical foundations, through all aspects of rough set theory and its applications, such as data mining, knowledge discovery, and intelligent information processing, to relations between rough sets and other approaches to uncertainty, vagueness, and incompleteness, such as fuzzy sets and theory of evidence. Volume VI of the Transactions on Rough Sets (TRS) commemorates the life and work of Zdzislaw Pawlak (19262006). His legacy is rich and varied. Prof. Pawlak's research contributions have had farreaching implications inasmuch as his works are fundamental in establishing new perspectives for scientific research in a wide spectrum of fields. This volume of the TRS presents papers that reflect the profound influence of a number of research initiatives by Professor Pawlak. In particular, this volume introduces a number of new advances in the foundations and applications of artificial intelligence, engineering, logic, mathematics, and science. These advances have significant implications in a number of research areas such as the foundations of rough sets, approximate reasoning, bioinformatics, computational intelligence, cognitive science, data mining, information systems, intelligent systems, machine intelligence, and security. 
.

2006  
[71] 
2006. Algebraic and Relational Deductive Tools. Conference Proceedings.
In series: Journal of Applied NonClassical Logics #??. Éditions HermèsLavoisier. Note: Special Issue 
.

[70] 
2006. On the fixpoint theory of equality and its applications. In Proceedings of the 9th International Conference on Relational Methods in Computer Science and 4th International Workshop on Applications of Kleene Algebra (RelMiCS/AKA), pages 388–401. In series: Lecture Notes in Computer Science #4136. Springer. DOI: 10.1007/11828563_26. In the current paper we first show that the fixpoint theory of equality is decidable. The motivation behind considering this theory is that secondorder quantifier elimination techniques based on a theorem given in [16], when successful, often result in such formulas. This opens many applications, including automated theorem. proving, static verification of integrity constraints in databases as well as reasoning with weakest sufficient and strongest necessary conditions. 
.

[69] 
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. 
.

[68] 
2006. Quantifier Elimination in Elementary Set Theory. In W. MacCaull, I. Duentsch, M. Winter, editors, Proceedings of the 8th International Conference on Relational Methods in Computer Science (RelMiCS), pages 237–248. In series: Lecture Notes in Computer Science #3929. Springer Berlin/Heidelberg. DOI: 10.1007/11734673_19. In the current paper we provide two methods for quantifier elimination applicable to a large class of formulas of the elementary set theory. The first one adapts the Ackermann method [1] and the second one adapts the fixpoint method of [20]. We show applications of the proposed techniques in the theory of correspondence between modal logics and elementary set theory. The proposed techniques can also be applied in an automated generation of proof rules based on the semanticbased translation of axioms of a given logic into the elementary set theory. 
.

[67] 
2006. Knowledge Representation Techniques.: a rough set approach. Book.
In series: Studies in Fuzziness and Soft Computing #202. Springer. 342 pages. ISBN: 9783540335184, 3540335188. DOI: 10.1007/3540335196. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/hitlist?d=libris&q=9... The basis for the material in this book centers around a long term research project with autonomous unmanned aerial vehicle systems. One of the main research topics in the project is knowledge representation and reasoning. The focus of the research has been on the development of tractable combinations of approximate and nonmonotonic reasoning systems. The techniques developed are based on intuitions from rough set theory. Efforts have been made to take theory into practice by instantiating research results in the context of traditional relational database or deductive database systems. This book contains a cohesive, selfcontained collection of many of the theoretical and applied research results that have been achieved in this project and for the most part pertain to nonmonotonic and approximate reasoning systems developed for an experimental unmanned aerial vehicle system used in the project. This book should be of interest to the theoretician and applied researcher alike and to autonomous system developers and software agent and intelligent system developers. 
.

[66] 
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. 
.

2005  
[65] 
2005. Similarity, approximations and vagueness. In Dominik Slezak, Guoyin Wang, Marcin S. Szczuka, Ivo Düntsch, Yiyu Yao, editors, Proceedings of the 10th International Conference on Rough Sets, Fuzzy Sets, Data Mining, and Granular Computing (RSFDGrC), pages 541–550. In series: Lecture Notes in Artificial Intelligence #3641. Springer. ISBN: 3540286535. DOI: 10.1007/11548669_56. The relation of similarity is essential in understanding and developing frameworks for reasoning with vague and approximate concepts. There is a wide spectrum of choice as to what properties we associate with similarity and such choices determine the nature of vague and approximate concepts defined in terms of these relations. Additionally, robotic systems naturally have to deal with vague and approximate concepts due to the limitations in reasoning and sensor capabilities. Halpern [1] introduces the use of subjective and objective states in a modal logic formalizing vagueness and distinctions in transitivity when an agent reasons in the context of sensory and other limitations. He also relates these ideas to a solution to the Sorities and other paradoxes. In this paper, we generalize and apply the idea of similarity and tolerance spaces [2,3,4,5], a means of constructing approximate and vague concepts from such spaces and an explicit way to distinguish between an agent’s objective and subjective states. We also show how some of the intuitions from Halpern can be used with similarity spaces to formalize the abovementioned Sorities and other paradoxes. 
.

[64] 
2005. A Technique for Learning Similarities on Complex Structures with Applications to Extracting Ontologies. In Proceedings of the 3rd Atlantic Web Intelligence Conference (AWIC), pages 991–995. In series: Lecture Notes in Computer Science #3528. Springer. DOI: 10.1007/11495772_29. A general similaritybased algorithm for extracting ontologies from data has been provided in [1]. The algorithm works over arbitrary approximation spaces, modeling notions of similarity and mereological partof relations (see, e.g., [2, 3, 4, 5]). In the current paper we propose a novel technique of machine learning similarity on tuples on the basis of similarities on attribute domains. The technique reflects intuitions behind tolerance spaces of [6] and similarity spaces of [7]. We illustrate the use of the technique in extracting ontologies from data. 
.

[63] 
2005. An Experimental Platform for Approximate Databases. In 3rd joint SAISSSL event on Artificial Intelligence and Learning Systems,2005. 
.

2004  
[62] 
2004. Towards a logical analysis of biochemical pathways. In José Júlio Alferes and João Alexandre Leite, editors, Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA), pages 667–679. In series: Lecture Notes in Computer Science #3229. Springer. ISBN: 9783540232421. DOI: 10.1007/9783540302278_55. Biochemical pathways or networks are generic representations used to model many different types of complex functional and physical interactions in biological systems. Models based on experimental results are often incomplete, e.g., reactions may be missing and only some products are observed. In such cases, one would like to reason about incomplete network representations and propose candidate hypotheses, which when represented as additional reactions, substrates, products, would complete the network and provide causal explanations for the existing observations. In this paper, we provide a logical model of biochemical pathways and show how abductive hypothesis generation may be used to provide additional information about incomplete pathways. Hypothesis generation is achieved using weakest and strongest necessary conditions which represent these incomplete biochemical pathways and explain observations about the functional and physical interactions being modeled. The techniques are demonstrated using metabolism and molecular synthesis examples. 
.

[61] 
2004. Towards a Logical Analysis of Biochemical Reactions (Extended abstract). In Ramon López de Mántaras, Lorenza Saitta, editors, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI), pages 997–998. IOS Press. ISBN: 1586034529. We provide a logical model of biochemical reactions and show how hypothesis generation using weakest sufficient and strongest necessary conditions may be used to provide additional information in the context of an incomplete model of metabolic pathways. 
.

[60] 
2004. Approximate Databases and Query Techniques for Agents with Heterogenous Perceptual Capabilities. In Proceedings of the 7th International Conference on Information Fusion, pages 175–182. ISIF. ISBN: 917056115X. In this paper, we propose a framework that provides software and robotic agents with the ability to ask approximate questions to each other in the context of heterogeneous and contextually limited perceptual capabilities. The framework focuses on situations where agents have varying ability to perceive their environments. These limitations on perceptual capability are formalized using the idea of tolerance spaces. It is assumed that each agent has one or more approximate databases where approximate relations are represented using intuitions from rough set theory. It is shown how sensory and other limitations can be taken into account when constructing approximate databases for each respective agent. Complex relations inherit the approximativeness inherent in the sensors and primitive relations used in their definitions. Agents then query these databases and receive answers through the filters of their perceptual limitations as represented by tolerance spaces and approximate queries. The techniques used are all tractable. 
.

[59] 
2004. On the Correspondence between Approximations and Similarity. In Shusaku Tsumoto, Roman Slowinski, Jan Komorowski and Jerzy W. GrzymalaBusse, editors, Proceedings of the International Conference on Rough Sets and Current Trends in Computing (RSCTC), pages 143–152. In series: Lecture Notes in Computer Science #3066. Springer. DOI: 10.1007/9783540259299_16. This paper focuses on the use and interpretation of approximate databases where both rough sets and indiscernibility partitions are generalized and replaced by approximate relations and similarity spaces. Similarity spaces are used to define neighborhoods around individuals and these in turn are used to define approximate sets and relations. There is a wide spectrum of choice as to what properties the similarity relation should have and how this affects the properties of approximate relations in the database. In order to make this interaction precise, we propose a technique which permits specification of both approximation and similarity constraints on approximate databases and automatic translation between them. This technique provides great insight into the relation between similarity and approximation and is similar to that used in modal correspondence theory. In order to automate the translations, quantifier elimination techniques are used. 
.

[58] 
2004. Approximative Query Techniques for Agents with Heterogeneous Ontologies and Perceptive Capabilities. In Didier Dubois, Christopher A. Welty, MaryAnne Williams, editors, Proceedings of the 9th International Conference on the Principles of Knowledge Representation and Reasoning, pages 459–468. AAAI Press. ISBN: 9781577351993. In this paper, we propose a framework that provides software and robotic agents with the ability to ask approximate questions to each other in the context of heterogeneous ontologies and heterogeneous perceptive capabilities.The framework combines the use of logicbased techniques with ideas from approximate reasoning. Initial queries by an agent are transformed into approximate queries using weakest sufficient and strongest necessary conditions on the query and are interpreted as lower and upper approximations on the query. Once the base communication ability is provided, the framework is extended to situations where there is not only a mismatch between agent ontologies, but the agents have varying ability to perceive their environments. This will affect each agent’s ability to ask and interpret results of queries. Limitations on perceptive capability are formalized using the idea of tolerance spaces. 
.

[57] 
2004. Using Contextually Closed Queries for Local ClosedWorld Reasoning in Rough Knowledge Databases. In Andrzej Skowron,Lech Polkowski ,Sankar K Pal, editors, RoughNeural Computing: Techniques for Computing with Words, pages 219–250. In series: Cognitive Technologies #??. Springer. ISBN: 9783540430599, 3540430598. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/14144444 find book in another country/hitta boken i ett annat land: http://www.worldcat.org/title/roughneur... Soft computing comprises various paradigms dedicated to approximately solving realworld problems, e.g., in decision making, classification or learning; among these paradigms are fuzzy sets, rough sets, neural networks, and genetic algorithms.It is well understood now in the soft computing community that hybrid approaches combining various paradigms provide very promising attempts to solving complex problems. Exploiting the potential and strength of both neural networks and rough sets, this book is devoted to roughneurocomputing which is also related to the novel aspect of computing based on information granulation, in particular to computing with words. It provides foundational and methodological issues as well as applications in various fields. 
.

[56] 
2004. Approximation Transducers and Trees: A Technique for Combining Rough and Crisp Knowledge. In Andrzej Skowron,Lech Polkowski ,Sankar K Pal, editors, RoughNeural Computing: Techniques for Computing with Words, pages 189–218. In series: Cognitive Technologies #??. Springer. ISBN: 9783540430599, 3540430598. find book at a swedish library/hitta boken i ett svenskt bibliotek: http://libris.kb.se/bib/14144444 find book in another country/hitta boken i ett annat land: http://www.worldcat.org/search?qt=worldc... Soft computing comprises various paradigms dedicated to approximately solving realworld problems, e.g., in decision making, classification or learning; among these paradigms are fuzzy sets, rough sets, neural networks, and genetic algorithms.It is well understood now in the soft computing community that hybrid approaches combining various paradigms provide very promising attempts to solving complex problems. Exploiting the potential and strength of both neural networks and rough sets, this book is devoted to roughneurocomputing which is also related to the novel aspect of computing based on information granulation, in particular to computing with words. It provides foundational and methodological issues as well as applications in various fields. 
.

2003  
[55] 
2003. Knowledge Representation and Approximate Reasoning. Conference Proceedings.
In series: Fundamenta Informaticae #2003(57):24. IOS Press. Note: Special Issue 
.

[54] 
2003. On a logical approach to estimating computational complexity of potentially intractable problems. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Proceedings of the 14th International Symposium on Fundamentals of Computation Theory (FCT), pages 423–431. In series: Lecture Notes in Computer Science #2751. Springer. DOI: 10.1007/9783540450771_39. In the paper we present a purely logical approach to estimating computational complexity of potentially intractable problems. The approach is based on descriptive complexity and secondorder quantifier elimination techniques. We illustrate the approach on the case of the transversal hypergraph problem, TRANSHYP, which has attracted a great deal of attention. The complexity of the problem remains unsolved for over twenty years. Given two hypergraphs, G and H, TRANSHYP depends on checking whether G = Hd, where Hd is the transversal hypergraph of H. In the paper we provide a logical characterization of minimal transversals of a given hypergraph and prove that checking whether G subset of or equal to Hd is tractable. For the opposite inclusion the Problem still remains open. However, we interpret the resulting quantifier sequences in terms of determinism and bounded nondeterminism. The results give better upper bounds than those known from the literature, e.g., in the case when hypergraph H, has a sublogarithmic number of hyperedges and (for the deterministic case) all hyperedges have the cardinality bounded by a function sublinear wrt maximum of sizes of G and H. 
.

[53] 
2003. 1st International Workshop on Knowledge Representation and Approximate Reasoning (KR&AR). 
.

[52] 
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. 
.

[51] 
2003. On mutual understanding among communicating agents. In B. DuninKeplicz and R. Verbrugge, editors, Proceedings of the International Workshop on Formal Approaches to MultiAgent Systems (FAMAS), pages 83–97. 
.

[50] 
2003. Tolerance Spaces and Approximative Representational Structures. In Proceedings of the 26th German Conference on Artificial Intelligence (KI), pages 475–489. In series: Lecture Notes in Computer Science #2821. Springer. DOI: 10.1007/9783540394518_35. In traditional approaches to knowledge representation, notions such as tolerance measures on data, distance between objects or individuals, and similarity measures between primitive and complex data structures are rarely considered. There is often a need to use tolerance and similarity measures in processes of data and knowledge abstraction because many complex systems which have knowledge representation components such as robots or software agents receive and process data which is incomplete, noisy, approximative and uncertain. This paper presents a framework for recursively constructing arbitrarily complex knowledge structures which may be compared for similarity, distance and approximativeness. It integrates nicely with more traditional knowledge representation techniques and attempts to bridge a gap between approximate and crisp knowledge representation. It can be viewed in part as a generalization of approximate reasoning techniques used in rough set theory. The strategy that will be used is to define tolerance and distance measures on the value sets associated with attributes or primitive data domains associated with particular applications. These tolerance and distance measures will be induced through the different levels of data and knowledge abstraction in complex representational structures. Once the tolerance and similarity measures are in place, an important structuring generalization can be made where the idea of a tolerance space is introduced. Use of these ideas is exemplified using two application domains related to sensor modeling and communication between agents. 
.

[49] 
2003. Information Granules for Intelligent Knowledge Structures. In Guoyin Wang, Qing Liu, Yiyu Yao, Andrzej Skowron, editors, Proceedings of the 9th International Conference on Rough Sets, Fuzzy Sets, Data Mining and Granular Computing (RSFDGrC), pages 405–412. In series: Lecture Notes in Computer Science #2639. Springer. ISBN: 9783540140405. DOI: 10.1007/354039205X_68. The premise of this paper is that the acquisition, aggregation, merging and use of information requires some new ideas, tools and techniques which can simplify the construction, analysis and use of what we call ephemeral knowledge structures. Ephemeral knowledge structures are used and constructed by granular agents. Each agent contains its own granular information structure and granular information structures of agents can be combined together. The main concept considered in this paper is an information granule. An information granule is a concise conceptual unit that can be integrated into a larger information infrastructure consisting of other information granules and dependencies between them. The novelty of this paper is that it provides a concise and formal definition of a particular view of information granule and its associated operators, as required in advanced knowledge representation applications. 
.

2002  
[48] 
2002. Secondorder quantifier elimination in modal contexts. In Sergio Flesca, Sergio Greco, Nicola Leone, Giovambattista Ianni, editors, Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA), pages 223–232. In series: Lecture Notes in Computer Science #2424. Springer. ISBN: 9783540441908. DOI: 10.1007/3540457577_19. 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 generalize the result of [19] by allowing modal operators. This allows us to provide a unifying framework for many applications, that require the use of intensional concepts. Examples of applications of the technique in AI are also provided. 
.

[47] 
2002. CAKE: A computer aided knowledge engineering technique. In Frank van Harmelen, editor, Proceedings of the 15th European Conference on Artificial Intelligence,2002, pages 220–224. IOS Press. Introduction: Logic engineering often involves the development of modeling tools and inference mechanisms (both standard and nonstandard) which are targeted for use in practical applications where expressiveness in representation must be traded off for efficiency in use. Some representative examples of such applications would be the structuring and querying of knowledge on the semantic web, or the representation and querying of epistemic states used with softbots, robots or smart devices. In these application areas, declarative representations of knowledge enhance the functionality of such systems and also provide a basis for insuring the pragmatic properties of modularity and incremental composition. In addition, the mechanisms developed should be tractable, but at the same time, expressive enough to represent such aspects as default reasoning, or approximate or incomplete representations of the environments in which the entities in question are embedded or used, be they virtual or actual. [...] 
.

2001  
[46] 
2001. On a Static Approach to Verification of Integrity Constraints in Relational Databases. In Eva Orlowska, Andrzej Szalas, editors, Relational Methods for Computer Science Applications, pages 97–109. In series: Studies in Fuzziness and Soft Computing #65. Springer PhysicaVerlag. ISBN: 3790813656. Find book at a Swedish library/Hitta boken i ett svenskt bibliotek: http://libris.kb.se/hitlist?d=libris&q=3... Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q=37908... 
.

[45] 
2001. Relational Methods for Computer Science Applications. In series: Studies in Fuziness and Soft Computing #??. Springer Physica Verlag. 297 pages. ISBN: 3790813656, 9783790813654. Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q=379081... This volume addresses all current aspects of relational methods and their applications in computer science. It presents a broad variety of fields and issues in which theories of relations provide conceptual or technical tools. The contributions address such subjects as relational methods in programming, relational constraints, relational methods in linguistics and spatial reasoning, relational modelling of uncertainty. All contributions provide the readers with new and original developments in the respective fields.The reader thus gets an interdisciplinary spectrum of the state of the art of relational methods and implementationoriented solutions of problems related to these areas 
.

[44] 
2001. Computing strongest necessary and weakest sufficient conditions of firstorder formulas. In 17th International Joint Conference on Artificial Intelligence,2001, pages 145–151. Morgan Kaufmann Publishers Inc.. ISBN: 1558608125, 9781558608122. A technique is proposed for computing the weakest sufficient (wsc) and strongest necessary (snc) conditions for formulas in an expressive fragment of firstorder logic using quantifier elimination techniques. The efficacy of the approach is demonstrated by using the techniques to compute snc's and wsc's for use in agent communication applications, theory approximation and generation of abductive hypotheses. Additionally, we generalize recent results involving the generation of successor state axioms in the propositional situation calculus via snc's to the firstorder case. Subsumption results for existing approaches to this problem and a reinterpretation of the concept of forgetting as a process of quantifier elimination are also provided. 
.

2000  
[43] 
2000. Algorithms based on Symbolic Transformations of Logical Formulas in the RDL Language. In Proceedings of the 2nd Conference on Applications of Computer Science in Mathematics and Economy, pages 101–115. WSIiE, Olsztyn, Poland. 
.

[42] 
2000. On RuleBased Approach to the Construction of Logical Transformers. In Proceedings of the 1st International Workshop on RuleBased Programming (RULE), pages 57–71. Springer PhysicaVerlag. 
.

[41] 
2000. Efficient reasoning using the local closedworld assumption. In Proceedings of the 9th International Conference on Artificial Intelligence: Methodology, Systems and Applications (AIMSA), pages 49–58. In series: Lecture Notes in Computer Science #1904. Springer Berlin/Heidelberg. ISBN: 9783540410447 (print), 9783540453314 (online). DOI: 10.1007/3540453318_5. We present a sound and complete, tractable inference method for reasoning with localized closed world assumptions (LCWA’s) which can be used in applications where a reasoning or planning agent can not assume complete information about planning or reasoning states. This <em>Open World Assumption</em> is generally necessary in most realistic robotics applications. The inference procedure subsumes that described in Etzioni et al [9], and others. In addition, it provides a great deal more expressivity, permitting limited use of negation and disjunction in the representation of LCWA’s, while still retaining tractability. The ap proach is based on the use of circumscription and quantifier elimination techniques and inference is viewed as querying a deductive database. Both the preprocessing of the database using circumscription and quan tifier elimination, and the inference method itself, have polynomial time and space complexity. 
.

1999  
[40] 
1999. Elimination of Predicate Quantifiers. In Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, Part I, pages 159–181. Kluwer Academic Publishers. 
.

[39] 
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. 
.

[38] 
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  
[37] 
1998. Wnioskowanie w logikach nieklasycznych: Automatyzacja wnioskowania. Book.
Academic Pub. PLJ (Akademicka Oficyna Wydawnicza PLJ). 159 pages. ISBN: 8371014031, 9788371014031. Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q=837101... 
.

[36] 
1998. A Fixpoint Approach to SecondOrder Quantifier Elimination with Applications to Correspondence Theory. In Ewa Orlowska, editor, Logic at work: essays dedicated to the memory of Helena Rasiowa, pages 307–328. In series: Studies in Fuzziness and Soft Computing #24. Physica Verlag. ISBN: 3790811645. Find book at a Swedish library/Hitta boken i ett svenskt bibliotek: http://libris.kb.se/hitlist?d=libris&q=3... Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q=37908... 
.

[35] 
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  
[34] 
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  
[33] 
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 
.

[32] 
1996. Proceedings of the 21st International Symposium on Mathematical Foundations of Computer Science (MFCS). Conference Proceedings.
In series: Lecture Notes in Computer Science #1113. Springer Verlag. ISBN: 9783540615507. Link: http://www.springer.com/computer/foundat... 
.

[31] 
1996. Declarative ptime queries to relational databases. Technical Report.
In series: LITHIDAR #34. Department of Computer and Information Science, Linköping University. 
.

[30] 
1996. General domain circumscription and its firstorder reduction. Technical Report.
In series: LITHIDAR #1. Department of Computer and Information Science, Linköping University. 
.

[29] 
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. 
.

[28] 
1996. Explaining explanation closure. In Zbigniew W. Ras, Maciek Michalewicz, editors, Proceedings of the 9th International Symposium on Methodologies for Intelligent Systems,1996, pages 521–530. In series: Lecture Notes in Computer Science #1079. Springer Berlin/Heidelberg. ISBN: 3540612866. DOI: 10.1007/3540612866_176. Recently, Haas, Schubert, and Reiter, have developed an alternative approach to the frame problem which is based on the idea of using <em>explanation closure axioms</em>. The claim is that there is a monotonic solution for characterizing nonchange in serial worlds with fully specified actions, where one can have both a succinct representation of frame axioms and an effective proof theory for the characterization. In the paper, we propose a circumscriptive version of explanation closure, PMON, that has an effective proof theory and works for both context dependent and nondeterministic actions. The approach retains representational succinctness and a large degree of elaboration tolerance, since the process of generating closure axioms is fully automated and is of no concern to the knowledge engineer. In addition, we argue that the monotonic/nonmonotonic dichotomy proposed by others is not as sharp as previously claimed and is not fully justified. 
.

[27] 
1996. General domain circumscription and its firstorder reduction. In Dov Gabbay, Hans Olbach, editors, Proceedings of the 1st International Conference on Formal and Applied Practical Reasoning (FAPR), pages 93–109. In series: Lecture Notes in Computer Science #1085. Springer Berlin/Heidelberg. ISBN: 9783540613138. DOI: 10.1007/3540613137_65. 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 isolate a class of domain circumscribed theories, such 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. 
.

1995  
[26] 
1995. Time and Logic: A Computational Approach. CRC Press. 325 pages. ISBN: 1857282337, 9781857282337. Find book at a Swedish library/Hitta boken i ett svenskt bibliotek: http://libris.kb.se/hitlist?d=libris&q= ... Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q= 97818... Time and logic are central driving concepts in science and technology. In this book, some of the major current developments in our understanding and application of temporal logic are presented in computational terms. \"Time and Logic: A Computational Approach\" should be a useful sourcebook for those within the specific field of temporal logic, as well as providing valuable introductory material for those seeking an entry into this increasingly important area of theoretical computing.; The emphasis of the book is on presenting a broad range of approaches to computational applications. The techniques used will also be applicable in many cases to formalize beyond temporal logic alone, and it is hoped that adaptation to many different logics of programmes will be facilitated. Throughout, the authors have kept implementationoriented solutions in mind.; The book begins with an introduction to the basic ideas of temporal logic. Successive chapters then examine particular aspects of the temporal theoretical computing domain, relating their applications to familiar areas of research, such as stochastic process theory, automata theory, established proof systems, model checking, relational logic and classical predicate logic. This should be a useful addition to the library of all theoretical computer scientists, providing a synthesis of well established results in temporal logic with the most uptodate findings of some of the world's leading theoreticians. 
.

[25] 
1995. Temporal Logic: A Standard Approach. In Leonard Bolc, Andrzej Szalas, editors, Time And Logic: A Computational Approach, pages 1–50. UCL Press Ltd.. ISBN: 1857282337, 9781857282337. Find book at a Swedish library/Hitta boken i ett svenskt bibliotek: http://libris.kb.se/hitlist?d=libris&q=1... Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q=978185... 
.

[24] 
1995. Wnioskowanie w logikach nieklasycznych: Podstawy teoretyczne. Book.
Academic Pub. PLJ (Akademicka Oficyna Wydawnicza PLJ). 247 pages. ISBN: 9788371012884. Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q=9788371... Prezentowana książka stanowi drugi tom dwutomowej monografii poświeconej wnioskowaniu w logikach nieklasycznych. Opracowanie to obejmuje takie formalizmy jak logiki modalne, logiki wielowartościowe i mechanizmy wnioskowania niemonotonicznego. W pierwszym tomie przedstawione zostały podstawy teoretyczne wnioskowania w wybranych logikach nieklasycznych. Tom drugi poświęcony jest zagadnieniom automatyzacji procesu wnioskowania. 
.

[23] 
1995. A characterization result for circumscribed normal logic programs. Revised version accepted for publication: Special issue of honor of H. Rasiowa, Fundamenta Informaticae. Technical Report.
In series: LITHIDAR #20. Department of Computer and Information Science, Linköping University. 
.

[22] 
1995. Computing circumscription revisited. In Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI), pages 1502–1508. ISBN: 9781558603639. Note: Volume 2. Preliminary report 
.

1994  
[21] 
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. 
.

[20] 
1994. Genetic Algorithms for Decision Problems. In Proceedings of the 6th International Conference on Artificial Intelligence and InformationControl Systems of Robots (AIICSR), pages 383–390. World Scientific. ISBN: 981021877X. 
.

[19] 
1994. Computing circumscription revisited: A reduction algorithm. Technical Report.
In series: LITHIDAR #9442. Department of Computer and Information Science, Linköping University. 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 ndorder 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, ndorder formulas into equivalent 1storder 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 which can be used in an algorithmic manner to reduce circumscription axioms to 1storder formulas. The algorithm takes as input an arbitrary 2ndorder formula and either returns as output an equivalent 1storder formula, or terminates with failure. The class of 2ndorder formulas, and analogously the class of circumscriptive theories which 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 and compare it with existing approaches providing formal subsumption results. 
.

1993  
[18] 
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  
[17] 
1992. Axiomatizing Fixpoint Logics. 
.

[16] 
1992. Zarys dedukcyjnych metod automatycznego wnioskowania. Book.
Academic Pub. RM (Akademicka Oficyna Wydawnicza RM). 120 pages. ISBN: 8390045176, 9788390045177. 
.

1991  
[15] 
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. 
.

[14] 
1991. Loglan. Book.
Wydawnictwa NaukowoTechniczne WNT. 172 pages. ISBN: 8320412951, 9788320412956. Note: In Polish; Volume 78, Biblioteka Inżynierii Oprogramowania Find book in another country/Hitta boken i ett annat land: http://www.worldcat.org/search?q=832041... 
.

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

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

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

[10] 
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. 
.

[9] 
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  
[8] 
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. 
.

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

[6] 
1987. A Compositional Method for the Design and Proof of Asynchronous Processes. In Proceedings of the 4th Annual ESPRIT Conference (ESPRIT), pages 566–580. NorthHolland. ISBN: 0444703330. 
.

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. 
.