Journal:Informatica
Volume 25, Issue 4 (2014), pp. 541–550
Abstract
Abstract
Terminating procedure GS-LCK-PROC of the proof search in the sequent calculus GS-LCK of logic of correlated knowledge is presented in this paper. Also decidability of logic of correlated knowledge is proved, where GS-LCK-PROC is a decision procedure.
Journal:Informatica
Volume 19, Issue 2 (2008), pp. 161–190
Abstract
In this paper, a new multi-criteria decision-making procedure is presented, which captures preferential information in the form of the threshold model. It is based on the ELECTRE-like sorting analysis restricted by the localization principle, which enables high adaptability of the decision model and reduces the cognitive load imposed on the decision-makers. It lays the foundation for the introduction of three concepts that have been previously insufficiently supported by outranking methods – semiautomatic derivation of criteria weights according to the selective effects of discordance and veto thresholds, convergent group consensus seeking, and autonomous multi-agent negotiation. The interdependent principles are justified, and the methodological solutions underlying their implementation are provided.
Journal:Informatica
Volume 18, Issue 1 (2007), pp. 103–114
Abstract
In this paper we consider branching time temporal logics of knowledge and belief. These logics involve the discrete time linear temporal logic operators “next” and “until” with the branching temporal logic operator “on all paths”. The latter operator is interpreted with respect to a version of the bundle semantics. In addition the temporal logic of knowledge (belief) contains an indexed set of unary modal operators “agent i knows” (“agent i believes”) and it contains the modality of common knowledge (belief). For these logics we present sequent calculi with a restricted cut rule. Thus, we get proof systems where proof-search becomes decidable. The soundness and completeness for these calculi are proved.
Journal:Informatica
Volume 17, Issue 1 (2006), pp. 39–54
Abstract
The asynchronous techniques that exist within the programming with distributed constraints are characterized by the occurrence of the nogood values during the search for the solution. The nogood type messages are sent among the agents with the purpose of realizing an intelligent backtrack and of ensuring the algorithm's completion.
In this article we analyzed the way in which a technique of obtaining efficient nogood values could combine with a technique of storing these values. In other words we try combining the resolvent-based learning technique introduced by Yokoo with the nogood processor technique in the case of asynchrounous weak-commitment search algorithm (AWCS). These techniques refer to the possibility of obtaining efficient nogoods, respectively to the way the nogood values are stored and the later use of information given by the nogoods in the process of selecting a new value for the variables associated to agents. Starting from this analysis we proposed certain modifications for the two known techniques.
We analyzed the situations in which the nogoods are distributed to more nogood processors handed by certain agents. We proposed a solution of distributing the nogood processors to the agents regarding the agents' order, with the purpose of reducing the storing and searching costs. We also analyzed the benefits the combining of nogood processor technique with the resolved-based learning technique could bring to the enhancement of the performance of AWCS technique. Finally, we analyzed the behavior of the techniques obtained in the case of messages filtering.
Journal:Informatica
Volume 15, Issue 3 (2004), pp. 379–398
Abstract
A temporal logic of belief and actions (TLBA) is considered. The TLBA allows us to express informational and dynamic properties of computational agents. The considered fragment of TLBA allows one: (1) to present a deduction‐based structured decision procedure; (2) to separate a decision procedure for so‐called induction‐free formulas and (3) to use only logical axioms for such formulas. The main new technical tool of the presented decision procedure is separation rules which incorporate traditional rules for the temporal operator “next”, belief modalities and action constants.