Meta-Reasoning in Executable Temporal Logic

Temporal logic can be used as a programming language. If temporal formulae are represented in the form of an implication where the antecedent refers to the past, and the consequent refers to the present and the future, then formulae that have their antecedent satisfied can be satisfied by considering the consequent as an imperative to be obeyed. Such a language becomes a natural alternative to programming languages, such as Prolog, for temporal reasoning. Here, the approach is extended to include an executable metalanguage. This is of importance in developing interpretation, debugging, loop-checking, and simulation tools, and provides a representation for providing control knowledge in the execution of planning and scheduling programs. 1 Executable Temporal Logic The traditional view of temporal logic is that it represents declarative statements about the world, or about possible worlds over time. Such statements relate the truth of propositions in the past, present and future, and ...

• Type: Conference
• Year: 1991
• Where: KR
• Authors: Howard Barringer, Michael Fisher, Dov M. Gabbay, Anthony Hunter
• Keywords: Automated Reasoning, KR 1991, Programming Languages, Temporal Formulae, Temporal Logic