# Deductive Algorithmic Knowledge

@article{Pucella2004DeductiveAK, title={Deductive Algorithmic Knowledge}, author={Riccardo Pucella}, journal={J. Log. Comput.}, year={2004}, volume={16}, pages={287-309} }

The framework of algorithmic knowledge assumes that agents use algorithms to compute the facts they explicitly know. In many cases of interest, a deductive system, rather than a particular algorithm, captures the formal reasoning used by the agents to compute what they explicitly know. We introduce a logic for reasoning about both implicit and explicit knowledge with the latter defined with respect to a deductive system formalizing a logical theory for agents. The highly structured nature of… Expand

#### Topics from this paper

#### 33 Citations

Belief ascription under bounded resources

- Computer Science
- Synthese
- 2009

This paper presents a formal model of a system of bounded reasoners which reason about each other’s beliefs, and investigates the problem of belief ascription in a resource-bounded setting, showing that for agents whose computational resources and memory are bounded, correct ascription of beliefs cannot be guaranteed, even in the limit. Expand

Knowledge and Security

- Computer Science
- ArXiv
- 2013

This survey illustrates some of these uses of epistemic concepts in security research by focusing on confidentiality in the context of cryptographic protocols, and in thecontext of multi-level security systems. Expand

Biometric Systems Private by Design: Reasoning about privacy properties of biometric system architectures

- Computer Science
- Trans. Data Priv.
- 2018

This work aims to show the applicability, and how, of privacy by design approach to biometric systems and the benefit of using formal methods to this end, and to explain how a general framework for the definition of privacy architectures can be adapted to biometrics. Expand

Reasoning About Privacy Properties of Architectures Supporting Group Authentication and Application to Biometric Systems

- Engineering, Computer Science
- DBSec
- 2016

This paper proposes an extension of an existing formal framework motivated by the need to reason about properties of architectures including group authentication functionalities, and shows that this extended framework can be used toreason about privacy properties of a biometric system in which users are authenticated through the use of group signatures. Expand

Formal Verification of Privacy Properties in Electric Vehicle Charging

- Computer Science
- ESSoS
- 2015

This paper provides a formal model of the expected privacy properties in the applied Pi-Calculus and uses ProVerif to check them, and identifies weaknesses in the protocol and suggest improvements to address them. Expand

Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System Architectures

- Computer Science
- FM
- 2015

It is shown that a general framework for the definition of privacy architectures can be used to specify these options and to reason about them in a formal way. Expand

Reasoning about Privacy Properties of Biometric Systems Architectures in the Presence of Information Leakage

- Computer Science
- ISC
- 2015

The existing formal model is extended in order to deal with side-channel attacks on biometric systems and the extended model is applied to analyse biometric information leakage in several variants of a biometric system architecture. Expand

Privacy Architectures: Reasoning about Data Minimisation and Integrity

- Computer Science
- STM
- 2014

This work proposes an approach based on the specification of privacy architectures and focus on a key aspect of privacy, data minimisation, and its tension with integrity requirements. Expand

Privacy by Design: From Technologies to Architectures - (Position Paper)

- Computer Science
- APF
- 2014

This paper advocates the idea that privacy by design should also be addressed at the architectural level and be associated with suitable methodologies, and believes that formal methods should play a key role in this area. Expand

The interrogative model of inquiry meets dynamic epistemic logics

- Computer Science
- Synthese
- 2014

A formal system called DEL is developed which aims to represent the interaction between question and inference dynamics in inquiry—as described by the IMI—in a multi-agent setting, and this in such a way as to enable an investigation of inquiry games with multi- agent dimensions. Expand

#### References

SHOWING 1-10 OF 40 REFERENCES

The computational complexity of prova

- 1977

A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief

- Mathematics, Computer Science
- Artif. Intell.
- 1992

It is shown that while the problem of deciding satisfiability of an S5 formula with one agent is NP-complete, the problem for many agents is PSPACE-complete and the problem becomes complete for exponential time once a common knowledge operator is added to the language. Expand

Deductive Algorithmic Knowledge.

- 2004

Probabilistic algorithmic knowledge

- Computer Science
- TARK '03
- 2003

The framework of algorithmic knowledge assumes that agents use deterministic knowledge algorithms to compute the facts they explicitly know; this work extends this framework to allow for randomized knowledge algorithms, and formalizes this information in terms of evidence. Expand

Modeling adversaries in a logic for reasoning about security protocols

- 2002

Modeling adversaries in a logic for reasoning about security protocols

- Proc . Workshop on Formal Aspects of Security ( FASec ’ 02 ) , Volume 2629 of Lecture Notes in Computer Science
- 2002

On a theory of probab

- 2001

On a theory of probabilistic deductive databases

- Computer Science
- Theory and Practice of Logic Programming
- 2001

This work develops a framework for probabilistic deductive databases by associating confidence levels with the facts and rules of a classical deductive database, and identifies a large natural class of query programs of practical interest in this framework. Expand

A computational model of belief

- Computer Science
- Artif. Intell.
- 2000

A logic of belief is proposed in which the expansion of beliefs beyond what has been explicitly learned is modeled as a finite computational process and it is shown that as long as the mechanism meets a particular set of constraints, the resulting logic has certain desirable properties. Expand

Reconciling two views of cry

- 2000