Tango: Declarative Semantics for Multiagent Communication Protocols

A flexible communication protocol is necessary to build a decentralized multiagent system whose member agents are not coupled to each other's decision making. Information-based protocol languages capture a protocol in terms of causality and integrity constraints based on the information exchanged by the agents. Thus, they enable highly flexible enactments in which the agents proceed asynchronously and messages may be arbitrarily reordered. However, the existing semantics for such languages can produce a large number of protocol enactments, which makes verification of a protocol property intractable. This paper formulates a protocol semantics declaratively via inference rules that determine when a message emission or reception becomes enabled during an enactment, and its effect on the local state of an agent. The semantics enables heuristics for determining when alternative extensions of a current enactment would be equivalent, thereby helping produce parsimonious models and yielding improved protocol verification methods.

Flexible coinductive logic programming

Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched by coclauses, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels.

Answer Set Programming with Composed Predicate Names

Mainstream systems for Answer Set Programming implement intelligent grounding to eliminate object variables from the input program, often obtaining a propositional program of reasonable size. However, non-stratified negation may inhibit the simplification of some rule bodies due to the lack of knowledge on the truth of recursive atoms. Frustration is greatest when the program is clearly locally stratified, such as in case of numerical arguments in rule heads obtained by increasing some body arguments; common examples are minimal distances in graphs and time arguments in planning scenarios. This paper suggests to move some arguments in predicate names, so that the declarative semantics of Answer Set Programming is preserved, but non-stratified negation is possibly avoided thanks to symbolic rule instantiation. A proof of concept is given in terms of Jinja templates for arguments with a clear range.

A Logic Framework for P2P Deductive Databases

This paper presents a logic framework for modeling the interaction among deductive databases in a peer-to-peer (P2P) environment. Each peer joining a P2P systemprovides or imports datafrom its neighbors by using a set ofmapping rules, that is, a set of semantic correspondences to a set of peers belonging to the same environment. By using mapping rules, as soon as it enters the system, a peer can participate and access all data available in its neighborhood, and through its neighborhood it becomes accessible to all the other peers in the system. A query can be posed to any peer in the system and the answer is computed by using locally stored data and all the information that can be consistently imported from the neighborhood. Two different types of mapping rules are defined: mapping rules allowing to import a maximal set of atoms not leading to inconsistency (calledmaximal mapping rules) and mapping rules allowing to import a minimal set of atoms needed to restore consistency (calledminimal mapping rules). Implicitly, the use of maximal mapping rules statesit is preferable to import as long as no inconsistencies arise; whereas the use of minimal mapping rules states thatit is preferable not to import unless a inconsistency exists. The paper presents three different declarative semantics of a P2P system: (i) theMax Weak Model Semantics, in which mapping rules are used to importas much knowledge as possiblefrom a peer’s neighborhood without violating local integrity constraints; (ii) theMin Weak Model Semantics, in which the P2P system can be locally inconsistent and the information provided by the neighbors is used to restore consistency, that is, to only integrate the missing portion of a correct, but incomplete database; (iii) theMax-Min Weak Model Semanticsthat unifies the previous two different perspectives captured by the Max Weak Model Semantics and Min Weak Model Semantics. This last semantics allows to characterize each peer in the neighborhood as a resource used either to enrich (integrate) or to fix (repair) the knowledge, so as to define a kind ofintegrate–repairstrategy for each peer. For each semantics, the paper also introduces an equivalent and alternative characterization, obtained by rewriting each mapping rule into prioritized rules so as to model a P2P system as a prioritized logic program. Finally, results about the computational complexity of P2P logic queries are investigated by consideringbraveandcautiousreasoning.

Hybrid Unification in the Description Logic EL

Unification in Description Logics (DLs) has been proposed as an inferenceservice that can, for example, be used to detect redundancies in ontologies.For the DL EL, which is used to define several largebiomedical ontologies, unification is NP-complete. However, the unification algorithms for EL developeduntil recently could not deal with ontologies containing general concept inclusions (GCIs).In a series of recent papers we have made some progress towards addressing this problem, but the ontologies thedeveloped unification algorithms can deal with need to satisfy a certain cycle restriction.In the present paper, we follow a different approach. Instead of restricting the input ontologies,we generalize the notion of unifiers to so-called hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes,hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics thatcombines fixpoint and declarative semantics. We show that hybrid unification in EL is NP-complete