Automated Deduction for a Multi-Modal Logic of Time and Knowledge

Olivier Gasquet

In this paper we expose how to reduce a logical problem to a unification problem, and present an algorithm which solves the latter. This algorithm computes a complete set of unifiers and terminates, thus we get a terminating, sound and complete theorem prover for the logic of knowledge and time we are interested in.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.