Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: formal frameworks

Sortuj według:

Ogranicz wyniki do:

Update of Probabilistic Beliefs: Implementation and Parametric Verification

Budzyńska K., Kacprzak M., Rembelski P.

Fundamenta Informaticae

2010

Vol. 102, nr 1

35-48

The aim of the paper is to propose how to enrich a formal model of persuasion with a specification for actions which are typical for persuasion process. First, since these actions are verbal, they influence a receiver but do not change the agent’s environment. In a formal framework, we represent them as actions that change not the particular state of a model, but the whole model. Second, effects of those actions depend on how much the receiver trusts the persuader. To formally model this phenomenon, we use a trust function. Finally, we want to represent uncertainty in terms of probability. Thus far, our model did not allow to express those properties of the persuasion process. Therefore, in this paper we extend Multimodal Logic of Actions and Graded Beliefs (AGn) with Probabilistic Dynamic Epistemic Logic (PDEL) and elements of Reputation Management framework (RM). Incorporation of PDEL into the model of persuasion requires some modifications of PDEL. Such extended model is then used to enrich Perseus - our software tool that enables to examine persuasive multi-agent systems. New components of the tool allow us to execute parametric verification of the different properties related to updating probabilistic beliefs in persuasion.

Specification and integration of theorem provers and computer algebra systems

Bertoli P.G., Calmet J., Giunchiglia F., Homann K.

Fundamenta Informaticae

1999

Vol. 39, Nr 1,2

39-57

Computer algebra systems (CASs) and automated theorem provers (ATPs) exhibit complementary abilities. CASs focus on efficiently solving domain-specific problems. ATPs are designed to allow for the formalization and solution of wide classes of problems within some logical framework. Integrating CASs and ATPs allows for the solution of problems of a higher complexity than those confronted by each class alone. However, most experiments conducted so far followed an ad-hoc approach, resulting in solutions tailored to specific problems. A structured and principled approach is necessary to allow for the sound integration of systems in a modular way. The Open Mechanized Reasoning Systems (OMRS) framework was introduced for the specification and implementation of mechanized reasoning systems, e.g. ATPs. In this paper, we introduce a generalization of OMRS, named OMSCS (Open Mechanized Symbolic Computation Systems). We show how OMSCS can be used to soundly express CASs, ATPs, and their integration, by formalizing a combination between the Isabelle prover and the Maple algebra system. We show how the integrated system solves a problem which could not be tackled by each single system alone.