We survey some general principles and methodologies for program analysis and verification. In particular, we focus on abstract interpretation and model checking techniques, and on their applications to constraint logic programs.
We review the Italian contribution to proof-theoretic and higher-order extensions of logic programming; this originated from the realization that Horn clauses lacked standard abstraction mechanisms such as higher-order programming, scoping constructs and forms of information hiding. Those extensions were based on the Deduction and Computation paradigm as formulated in Miller et al’s approach [51], which built logic programming around the notion of focused uniform proofs The Italian contribution has been both foundational and applicative, in terms of language extensions, implementation techniques and usage of the new features to capture various computation models. We argue that the emphasis has now moved to the theory and practice of logical frameworks, carrying with it a better understanding of the foundations of proof search.
In designing a large-scale computerized proof system, one is often confronted with issues of two kinds: issues regarding an underlying logical calculus, and issues that refer to theories, either specified axiomatically or characterized by indication of either a privileged model or a family of intended models. Proof services related to the theories most often take the form of satisfiability decision or semi-decision procedures (in a sense, polyadic inference rules), while some of the services offered by the calculus (e.g., the Davis-Putnam propositional satisfiability checker) provide low-level mechanisms for integrating services of the former kind. Integration among services can ensure speed-up (i.e., lower number of steps) in the proofs, but it must always be legitimatized by a conservativeness result. Interoperability among proof checkers and autonomous theorem provers is another key point of integration. In discussing these and related issues, this paper refers to Set Theory as the unifying background, and to a specific proof-checker based on a slightly unorthodox formalization of it as an arena for experimentation.
This chapter tackles the relation between declarative languages and multi-agent systems by following the dictates of the five Ws (and one H) that characterize investigations. The aim is to present this research field, which has a long-term tradition, and discuss about its future. The first question to answer is “What? What are declarative agents and multi-agent systems?”. Therefore, we will introduce the history of declarative agent systems up to the state of the art by answering the question “When? When did research on them begin?”. We will, then, move to the question “Where? Where can it take place?”: in which kind of real applications and for which kind of problems declarative agents and MAS have already proven useful? Connected to where is “Why? Why should it happen?”. We will discuss the benefits of adopting the abstractions offered by declarative approaches for developing communication, interaction, cooperation mechanisms. We will compare with other technologies, mainly service-based and object-oriented ones. “Who? Who can be involved?”: in order to exploit this kind of technology what sort of background does a specialist have to acquire? We address this question by looking at the Italian landscape of Computer Science research and education. Finally, with the question “How? How can it happen?” we will shortly report some examples of existing declarative languages and frameworks for the specification, verification, implementation and prototyping of agents and MAS.
This chapter contains a reference selection of Italian contributions in the intersection of Logic Programming (LP) with databases and the (Semantic) Web. More precisely, we will survey the main contributions on deductive databases such as the coupling of Prolog systems and database systems, evaluation and optimization techniques, Datalog extensions for expressing nondeterministic and aggregate queries, and active rules and their relation to deductive rules. Also we will illustrate solutions employing LP for querying the Web, manipulating Web pages, representing knowledge in the Semantic Web and learning Semantic Web ontologies and rules.
The history of Logic Programming in Italy is largely that of GULP, the Italian Association of Users and Researchers in Logic Programming. This paper provides a historical perspective on the birth and development of GULP in the last 25 years. The paper is mainly concerned with what has been done in Italy, but it also points out the many relationships and synergies that emerged-and still exist-in the field of Logic Programming, between Italy and other countries all over the world. I identify three main periods in the history of GULP, which closely correspond to different seasons in the history of Logic Programming in general, and I try to characterize them in terms of activities the GULP supported and of the achievements obtained by its members.
Logic programming has been deployed to support non-monotonic reasoning since the late '80s. In this paper, we review semantics, formalisms and computational mechanisms for logic programming for non-monotonic reasoning. We also discuss some formalisms that have emerged from the cross fertilization between the two areas and some applications in as diverse areas as reasoning about dynamic domains, security, diagnosis and legal reasoning.
We analyze the motto: "efficiency = parallelism + communications" as an approach for developing parallel programs. Communications are used for deriving suitable program transformations via definition of "eureka" functions or synthesis of "annotations". We also introduce a strategy, called minimal extension strategy, for obtaining new auxiliary functions, and some preliminary ideas for a new theory of communications, which do not effect program correctness, but only program efficiency.
The Italian Logic Programming community has given several contributions to the theory of Concurrent Constraint Programming. In particular, in the topics of semantics, verification, and timed extensions. In this paper we review the main lines of research and contributions of the community in this field.
We present a review of practical applications of Logic Programming appeared in Italy since 1985. We classify them according to their area of application and discuss some trends emerged in the latest developments. Notwithstanding this survey is far to be comprehensive, it shows that Logic Programming successfully evolved and quickly adapted to new challenges offered by a notable variety of application areas.
The Italian contribution to functional-logic programming has been significant and influential in a number of areas of semantics, and semantics-based program manipulation techniques. We survey selected topics, with a particular regard to debugging and transformation techniques. These results as usual depend on the narrowing strategy which is adopted and on the properties satisfied by the considered programs. In this paper, we restrict ourselves to first-order functional-logic languages without non-deterministic functions. We start by describing some basic classical transformation techniques, namely folding and unfolding. Then, we recall the narrowing-driven partial evaluation, which is the first generic algorithm for the specialization of functional logic programs. Regarding debugging, we describe a goal-independent approach to automatic diagnosis and correction which applies the immediate consequence operator modeling computed answers to the diagnosis of bugs in functional logic programs. A companion bug-correction program synthesis methodology is described that attempts to correct the erroneous components of the wrong code.
The paper provides an overview of an approach to the semantics of (constraint) logic programs, whose aim is providing suitable theoretical bases for modeling observable properties of logic programs in a compositional way. The approach is based on the idea of choosing (either equivalence classes or abstractions of) sets of clauses as semantic domain and provides an uniform framework for defining different compositional semantics for logic programs, parametrically with respect to a given notion of observability. Since some observable properties have a natural definition which is dependent on the selection rule, the framework has been adapted to cope also with a suitable class of rules, which includes the leftmost selection rule. This provides a formal description of most of the observable properties of Prolog derivations and can therefore be viewed as reference semantics for Prolog transformation and analysis systems.
Correction of OBJ-like Programs ? M. Alpuente, D. Ballis, S. Escobar, M. Falaschi, and S. Lucas 1 DSIC, Universidad Politecnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46071 Valencia, Spain. {alpuente,sescobar,slucas}@dsic.upv.es. 2 Dip. Matematica e Informatica, Via delle Scienze 206, 33100 Udine, Italy. {demis,falaschi}@dimi.uniud.it. Abstract. Debussy is an (abstract) declarative diagnosis tool for functional programs which are written in OBJ style. The debugger does not require the user to either provide error symptoms in advance or answer Debussy is an (abstract) declarative diagnosis tool for functional programs which are written in OBJ style. The debugger does not require the user to either provide error symptoms in advance or answer any question concerning program correctness. In this paper, we formalize an inductive learning methodology for repairing program bugs in OBJlike programs. Correct program rules are automatically synthesized from examples which might be generated as an outcome by the Debussy di-
In the context of Network management, Chomicki et al. defined the specification language PDL (Policy Description Language) and later extended it by introducing monitors: constraints on the actions that the network manager cannot execute simultaneously. We have furtherly extended PDL by permitting specifying user preferences on how to enforce constraints; that extension is called PPDL and it is based on Brewka’s ordered disjunction connective. In this article we speculate on how the minimality requirement, stating that constraints on actions should affect action execution as little as possible, can be specified and implemented in PPDL theories. Minimal interference and maximal satisfaction of user preferences are not always achievable and tend to interact in complex ways.
Disjunctive logic programs are a powerful tool in knowledge representation and commonsense reasoning. The recent development of an efficient disjunctive logic programming engine, named DLV, allows to exploit disjunctive logic programs for solving complex problems. However, disjunctive logic programming systems are currently missing any interface supporting the integration between commonly used software development languages (like Java or C++) and disjunctive logic programs. This paper focuses on the DLV Wrapper, a library, actually implemented in Java, that “wraps” the DLV system inside an external application, allowing to embed disjunctive logic programs inside Object-Oriented source code.
Ordered Choice Logic Programming (OCLP) allows for preferencebased decision-making with multiple alternatives without the burden of any form of negation. This complete absence of negation does not weaken the language as both forms (classical and as-failure) can be intuitively simulated in the language. The semantics of the language is based on the preference between alternatives, yielding both a skeptical and a credulous approach. In this paper we demonstrate how OCLPs can be translated to semi-negative logic programs such that, depending on the transformation, the answer sets of the latter correspond with the skeptical or credulous answer sets of the former. By providing such a mapping, we have a mechanism for implementing OCLP using an answer set solver like smodels or dlv.
Sommario In questo lavoro viene proposto un agente intelligente denominato DL-WBA (Description Logic based Web Browsing Assistant Agent) per supportare un utente nelle sue attività di browsing sul Web. L’attività di ricerca di nuove sorgenti informative è basata sull’utilizzo di un profilo utente che registra gli interessi e le preferenze dell’utente. Ogniqualvolta l’utente effettua una query, viene attivato un motore di ricerca classico per determinare un insieme (in generale abbastanza ampio) di sorgenti informative ad essa correlate. DL-WBA, utilizzando le informazioni memorizzate nel profilo utente, produce il sottoinsieme di sorgenti informative più “prossimo” ai desideri dell’utente. Al fine di confrontare il grado di affinità di una sorgente informativa con i contenuti del profilo utente viene definito e adottato un meccanismo inferenziale derivato da una variante probabilistica della Logica Descrittiva.
The Semantic Web (SW) can be seen as abstract representation and exchange of data and metadata. Metadata is given in terms of data mark-up and reference to shared, Web-accessible ontologies. Several interesting languages are now available for the Semantic Web. They exploit XML allowing data/metadata communication, yet are endowed with a logical semantics. Such languages allow compact descriptions by means of inheritance mechanisms that permit one to describe an object as belonging to one or more classes whose hierarchy is already described on the Web. With few exceptions, SW logical languages are designed to be monotonic, thus they cannot employ the closed-world assumption i) to make object description compact and most importantly ii) to prevent large ontologies from admitting inconsistency resulting from multiple inheritance. We address these problems by proposing a version of Local Closed-World Assumption that fits SW purposes. Its extent is itself the subject of negotiation between communicating agents. In this light, we give a new default semantics to RDF type inheritance primitives and show that Answer Set Programming seems a promising tool for the automation of consistency maintenance over Semantic Web annotations.
This paper is a presentation of ONTO-DLP, an extension of Disjunctive Logic Programming (DLP) for complex knowledge modelling. ONTO-DLP enhances DLP by constructs coming from other knowledge representation formalisms, namely, Complex-Datalog and Ordered Logic. The former provides suitable abstraction mechanisms for complex objects handling, while the latter provides support for default reasoning. Such features make ONTO-DLV a powerful language for ontology specification and reasoning.
