# 2005.bib

@article{AlbGavLam05-TPLP-IJ,
key = 001,
author = {Marco Alberti And Marco Gavanelli And Evelina Lamma And  Paola Mello And Michela Milano},
title = {A {CHR}-based implementation of known arc-consistency},
journal = {Theory and Practice of Logic Programming},
year = 2005,
volume = 5,
number = {4/5},
pages = {419-440},
month = jul,
http = {http://journals.cambridge.org/action/displayIssue?jid=TLP&volumeId=5&issueId=4-5},
doi = {http://dx.doi.org/10.1017/S147106840500236X},
abstract = {  In classical CLP(FD) systems, domains of variables are completely
known at the beginning of the constraint propagation process.
However, in systems interacting with an external environment, this
assumption may lead to waste of computation time, or even to
obsolescence of the acquired data at the time of use.

For such cases, the Interactive Constraint Satisfaction Problem
(ICSP) model has been proposed as an extension of the CSP model, to
make it possible to start constraint propagation even when domains are
not fully known, performing acquisition of domain elements only when
necessary and without the need to restart propagation after every
acquisition.

In this paper, we present a two sorted CLP language to express and
solve ICSPs, and its implementation in the Constraint Handling Rules
(CHR) language, a declarative language particularly suitable for
high level implementation of constraint solvers.},
issn = {1471-0684},
note = {IF: 1.372}
}

@inproceedings{AlbGavLam05-IJCAI-IC,
author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Abduction with hypotheses confirmation},
booktitle = {IJCAI-05 Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence},
year = {2005},
editor = {Fausto Giunchiglia},
pages = {1545--1546},
publisher = {Professional Book Center},
isbn = {0-938075-93-4},
url = {http://www.ing.unife.it/docenti/MarcoGavanelli/publications/poster-ijcai05.ppt},
pdf = {http://ijcai.org/papers/post-0385.pdf}
}

@article{AlbGavLam05-AIIA-IC,
author = {Marco Alberti and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {The \textit{S}{CIFF} abductive proof-procedure},
booktitle = {AI*IA 2005: Advances in Artificial Intelligence: 9th Congress of the Italian Association for Artificial Intelligence, Milan, Italy, September 21-32, 2005. Proceedings},
year = {2005},
editor = {Stefania Bandini and Sara Manzoni},
journal = {Lecture Notes in Artificial Intelligence},
publisher = {Springer Verlag},
pages = {135-147},
volume = {3673},
issn = {0302-9743},
abstract = {We propose an operational framework which builds on the classical
understanding of abductive reasoning in logic programming, and
extends it in several directions. The new features include the
ability to reason with a dynamic knowledge base, where new facts
such new facts occurring in the future (forecasting), and the
process of confirmation/disconfirmation of such expectations.},
note = {IF: 0.302}
}

@article{AlbCheGav05-GC-IW,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {The {SOCS} Computational Logic Approach to the Specification and Verification of Agent Societies},
booktitle = {Global Computing: {IST/FET} International Workshop, GC 2004 Rovereto, Italy, March 9-12, 2004 Revised Selected Papers},
year = {2005},
issn = {0302-9743},
month = feb,
editor = {Corrado Priami and Paola Quaglia},
journal = {Lecture Notes in Computer Science},
doi = {10.1007/b103251},
publisher = {Springer Verlag},
abstract = {This article summarises part of the work done during the first
two years of the SOCS project, with respect to the task of
modelling interaction amongst CL-based agents. It describes the
SOCS social model: an agent interaction specification and
verification framework equipped with a declarative and
operational semantics, expressed in terms of abduction. The
operational counterpart of the proposed framework has been
implemented and integrated in SOCS-SI, a tool that can be used
for on-the-fly verification of agent compliance with respect to
specified protocols.},
pages = {314 - 339},
volume = 3267,
note = {IF: 0.402}
}

@article{AlbChe05-IA-NJ,
author = {Marco Alberti and Federico Chesani},
title = {The computational behaviour of the {SCIFF} abductive proof procedure and the {SOCS-SI} system},
journal = {Intelligenza Artificiale},
year = 2005,
volume = {II},
number = 3,
pages = {45--51},
month = {September},
issn = {1724-8035},
abstract = {The high computational cost of abduction has limited the application
of this powerful and expressive formalism to practical cases.

SCIFF is an abductive proof procedure used for verifying the
compliance of agent behaviour to interaction protocols in multi-agent
systems; SCIFF has been integrated in SOCS-SI, a system able to
observe the agent interaction, pass it to SCIFF for the reasoning
process and to display in a GUI the results of the SCIFF
computation.

In order to assess the applicability of SCIFF and SOCS-SI to
practical cases, we have evaluated qualitatively and experimentally
(not yet formally) their computational behaviour, concerning
limitations and scalability. In this paper we show the results of
the analysis.}
}

@article{AlbCheGav05-IA-NJ,
author = {Marco Alberti and Federico Chesani and Marco Gavanelli and Alessio Guerri and Evelina Lamma and Paola Mello and Paolo Torroni},
title = {Expressing Interaction in Combinatorial Auction through Social Integrity Constraints},
journal = {Intelligenza Artificiale},
year = {2005},
pages = {22--29},
volume = {{II}},
number = {1},
abstract = {Combinatorial Auctions are an attractive
application of intelligent agents; their applications are
countless and are shown to provide good revenues. On the other
hand, one of the issues they raise is the computational complexity
of the solving process (the Winner Determination Problem, WDP),
that delayed their practical use. Recently, efficient solvers have
been applied to the WDP, so the framework starts to be viable.
%
A second issue, common to many other agent systems, is {\em
trust}: in order for an agent system to be used, the users must
{\em trust} both their representative and the other agents
inhabiting the society: malicious agents must be found, and their
violations discovered. The SOCS project addresses such issues, and
provided a language, the  social integrity constraints, for
defining the allowed interaction moves, together with a proof
procedure able to detect violations.
%
In this paper we show how to write a protocol for the
combinatorial auctions by using social integrity constraints. In
the devised protocol, the auctioneer interacts with an external
solver for the winner determination problem.},
issn = {1724-8035},
url = {http://ia.di.uniba.it/}
}

@inproceedings{CheCiaMel05-WOA-NW,
author = {Federico Chesani and
Anna Ciampolini and
Paola Mello and
Marco Montali and
Paolo Torroni and
Marco Alberti and
Sergio Storari},
title = {Protocol Specification and Verification by Using Computational Logic.},
Flavio De Paoli and
Emanuela Merelli and
Andrea Omicini},
booktitle = {WOA 2005: Dagli Oggetti agli Agenti. 6th AI*IA/TABOO Joint
Workshop "From Objects to Agents": Simulation and Formal
Analysis of Complex Systems, 14-16 November 2005, Camerino,
MC, Italy},
publisher = {Pitagora Editrice Bologna},
year = {2005},
isbn = {88-371-1590-3},
pages = {184-192},
ee = {http://lia.deis.unibo.it/books/woa2005/papers/26.pdf},
bibsource = {0DBLP, http://dblp.uni-trier.de},
abstract = {  The aim of this paper is to report on some preliminary results
obtained in the context of the MASSIVE research project
(http://www.di.unito.it/massive/) relating the formal
specification and verification of protocols in some different
application field. A protocol is a way to express the right behavior
of entities involved in a (possibly complex and distributed)
process. The formalism to be used for protocol description should be
as intuitive as possible, but it should be also formally defined, in
order to allow formal checks both on the features of the protocol
itself (e.g. termination), and also on the execution of it. To this
purpose, we will show some results obtained by exploiting the
SOCS-SI logic-based framework for the specification and the
verification of protocols in various applicative fields such as
electronic commerce, medicine and e-learning. We will also present a
new graphical notation to express medical guidelines, which could be
automatically translated into the SOCS formalism.}
}

@phdthesis{Alb05-PT,
author = {Marco Alberti},
title = {A Computational Logic-based System for Specification and Verification of Agent Interaction},
school = {University of Ferrara},
year = 2005,
month = {March},