Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)

The semantics of computational systems (e.g., relational and knowledge data bases, query-answering systems, programming languages, etc.) can often be expressed as (the specification of) a logical theory Th. Queries, goals, and claims about the behavior or features of the system can be expressed as formulas φ which should be checked with respect to the intended model of Th, which is often huge or even incomputable. In this paper we show how to prove such semantic properties φ of Th by just finding a model A of Th∪{φ}∪Zφ, where Zφ is an appropriate (possibly empty) theory depending on φ only. Applications to relational and deductive databases, rewriting-based systems, logic programming, and answer set programming are discussed.

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.

Deductive systems for BigData integration

The globalization is associated with an increased data to be processed from E-commerce transactions. The specialists are looking for different solutions, such as BigData, Hadoop, Datawarehoues, but it seems that the future is the predicative logic implemented through deductive database technology. It has to be done the swift from imperative languages, to not declaratively languages used for the application development. The deductive databases are very useful in the student teaching programs, too. Thus, the article makes a consistent literature review in the field and shows practical examples of using predicative logic in deductive systems, in order to integrate different kind of data types.