| 1. |
- Cantwell, John
(författare)
-
A model for updates in a multi-agent setting
- 2007
-
Ingår i: Journal of Applied Non-Classical Logics. - : Informa UK Limited. - 1166-3081 .- 1958-5780. ; 17:2, s. 183-196
-
Tidskriftsartikel (refereegranskat)
|
|
| 2. |
- Doherty, Patrick, 1957-, et al.
(författare)
-
Approximate Databases : A support tool for approximate reasoning
- 2006
-
Ingår i: Journal of applied non-classical logics. - : Éditions Hermès-Lavoisier. - 1166-3081 .- 1958-5780. ; 16:1-2, s. 87-118
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 3. |
- Dunin-Keplicz, Barbara, et al.
(författare)
-
Converse-PDL with Regular Inclusion Axioms : A Framework for MAS Logics
- 2011
-
Ingår i: Journal of Applied Non-Classical Logics. - Cachan, France : Lavoisier. - 1166-3081 .- 1958-5780. ; 21:1, s. 61-91
-
Tidskriftsartikel (refereegranskat)abstract
- 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 multi-agent 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 multi-agent 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 (Dunin-Kęplicz et al., 2010a). The main contribution are proofs of soundness and completeness of the tableau calculus for CPDLreg provided in (Dunin-Kęplicz et al., 2010a).
|
|
| 4. |
- Gabelaia, David, et al.
(författare)
-
Temporal logic of surjective bounded morphisms between finite linear processes
- 2024
-
Ingår i: Journal of Applied Non-Classical Logics. - : Taylor & Francis. - 1166-3081 .- 1958-5780. ; 34:1, s. 1-30
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we study temporal logic for finite linear structures and surjective bounded morphisms between them. We give a characterisation of such structures by modal formulas and show that every pair of linear structures with a bounded morphism between them can be uniquely characterised by a temporal formula up to an isomorphism. As the main result, we prove Kripke completeness of the logic with respect to the class of finite linear structures with bounded morphisms between them.
|
|
| 5. |
- Jonsson, Peter, 1969-
(författare)
-
Adding Clauses to Poor Man's Logic (Without Increasing the Complexity)
- 2005
-
Ingår i: Journal of applied non-classical logics. - : Informa UK Limited. - 1166-3081 .- 1958-5780. ; 15:3, s. 341-357
-
Tidskriftsartikel (refereegranskat)abstract
- Partly motivated by description logics, poor man's logics have been proposed as an interesting fragment of modal logics. A poor man's logic is a propositional modal logic where only literals and the connectives , , and are allowed. It is known that the complexity of the satisfiability problem may drop dramatically when going from a full modal logic to the corresponding poor man's logic, e.g., in the case of modal logic K one goes from PSPACEcomplete to coNP-complete. We prove that it is sometimes possible to extend poor man's logics with restricted disjunctions (i.e., clauses) without increasing the computational complexity. For Horn and Krom clauses, we provide necessary and sufficient conditions for when the resulting logic is polynomial-time. Such extensions correspond to allowing a restricted use of the union operator in description logics.
|
|
| 6. |
- Maluszynski, Jan, et al.
(författare)
-
Logical Foundations and Complexity of 4QL, a Query Language with Unrestricted Negation
- 2011
-
Ingår i: Journal of Applied Non-Classical Logics. - Cachan, France : Lavoisier. - 1166-3081 .- 1958-5780. ; 21:2, s. 211-232
-
Tidskriftsartikel (refereegranskat)abstract
- 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 four-valued 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:investigate properties of well-supported models of 4QLprove the correctness of the algorithm for computing well-supported modelsshow that 4QL has PTIME data complexity and captures PTIME.
|
|
| 7. |
- Szalas, Andrzej
(författare)
-
On an Automated Translation of Modal Proof Rules into Formulas of the Classical Logic
- 1994
-
Ingår i: Journal of Applied Non-Classical Logics. - : Éditions Hermès-Lavoisier. - 1166-3081 .- 1958-5780. ; 4:2, s. 119-127
-
Tidskriftsartikel (refereegranskat)abstract
- 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 second-order 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.
|
|
| 8. |
- Szalas, Andrzej, 1956-
(författare)
-
Second-order Reasoning in Description Logics
- 2006
-
Ingår i: Journal of applied non-classical logics. - : Éditions Hermès-Lavoisier. - 1166-3081 .- 1958-5780. ; 16:3 - 4, s. 517-530
-
Tidskriftsartikel (refereegranskat)abstract
- 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 second-order reasoning. One of the important motivations behind introducing second-order formalism follows from the fact that many forms of commonsense and nonmonotonic reasoning used in AI can be modelled within the second-order 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 second-order formalisms is their complexity, we next propose second-order 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.
|
|
| 9. |
- Szalas, Andrzej, 1956-
(författare)
-
Towards Incorporating Background Theories into Quantifier Elimination
- 2008
-
Ingår i: Journal of applied non-classical logics. - : Éditions Hermès-Lavoisier. - 1166-3081 .- 1958-5780. ; 18:2-3, s. 325-340
-
Tidskriftsartikel (refereegranskat)abstract
- In the paper we present a technique for eliminating quantifiers of arbitrary order, in particular of first-order. Such a uniform treatment of the elimination problem has been problematic up to now, since techniques for eliminating first-order quantifiers do not scale up to higher-order contexts and those for eliminating higher-order quantifiers are usually based on a form of monotonicity w.r.t implication (set inclusion) and are not applicable to the first-order case. We make a shift to arbitrary relations "ordering" the underlying universe. This allows us to incorporate background theories into higher-order 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.
|
|
| 10. |
|
|
