Automated deduction in a graphical temporal logic
作者:
L.E. Moser,
P.M. Melliar-Smith,
Y.S. Ramakrishna,
G. Kutty,
L.K. Dillon,
期刊:
Journal of Applied Non-Classical Logics
(Taylor Available online 1996)
卷期:
Volume 6,
issue 1
页码: 29-47
ISSN:1166-3081
年代: 1996
DOI:10.1080/11663081.1996.10510865
出版商: Taylor & Francis Group
关键词: automated deduction;Büchi automaton;graphical representation;interval logic;real-time;temporal logic
数据来源: Taylor
摘要:
Real-time graphical interval logic is a modal logic for reasoning about time in which the basic modality is the interval. The logic differs from other logics in that it has a natural intuitive graphical representation that resembles the timing diagrams drawn by system designers. We have developed an automted deduction system for the logic, which includes a theorem prover and a user interface. The theorem prover checks the validity of proofs in the logic and produces counterexamples to invalid proofs. The user interface includes a graphical editor that enables the user to create graphical formulas on a workstation display, and a database and proof manager that tracks proof dependencies and allows graphical formulas to be stored and retrieved. In this paper we describe the logic, the automated deduction system, and an application to robotics.
点击下载:
PDF (989KB)
返 回