Local deduction of trust
Anders M. Hagalisletto
Abstract:We explore how agents establish new beliefs about their environment and how trust can be used to guide the agents in a possible hostile environment. Two tracks are explored: First we show how the specifications can be translated into rewrite rules using epistemic logic as guiding principles in the design of the semantics. Second it is indicated how agents can be extended to autonomous theorem provers that do much of the work by themselves, resulting in a realistic logic for artificial agents. The operational semantics is embedded in a denotational semantics, capable of expressing secrecy properties of many kinds. Yet reasoning about trust necessarily involves second order quantification. The agents struggle with instantiation of universal quantification, in general a belief set might be non-terminating for any finite input given to the agent.
Keywords:
term rewriting, operational semantics, trust, local theorem proving, temporal epistemic logic, second order quantification, terminating deductions