The synthesis of digital machines with provable epistemic properties

摘要: Researchers using epistemic logic as a formal framework for studying knowledge properties of AI systems often interpret the formula K(x, φ) to mean that machine x encodes φ in its state syntactic or can derive it inferentially. By defining φ), instead, terms correlation between and environment, modal system S5 be satisfied without having store representations formulas data structures. In this paper, we apply correlational definition machines with composite structure. particular, describe how synchronous digital analyzed, starting at level gates delays, by modeling machine's components agents multi-agent reasoning about flow information among them. We also introduce Rex, language recursively computing descriptions, illustrate used construct provable properties.