2 December 2014 A computer method of finding valuations forcing validity of LC formulae
Author Affiliations +
Proceedings Volume 9290, Photonics Applications in Astronomy, Communications, Industry, and High-Energy Physics Experiments 2014; 92902X (2014) https://doi.org/10.1117/12.2075115
Event: Symposium on Photonics Applications in Astronomy, Communications, Industry and High-Energy Physics Experiments, 2014, Warsaw, Poland
Abstract
The purpose of this paper is to present the computer implementation of a system known as LC temporal logic [1]. Firstly, to become familiar with some theoretical issues, a short introduction to this logic is discussed. The algorithms allowing a deep analysis of the formulae of LC logic are considered. In particular we discuss how to determine if a formula is a tautology, contrtautology or it is satisfable. Next, we show how to find all valuations to satisfy the formula. Finally, we consider finding histories generated by the formula and transforming these histories into the state machine. Moreover, a description of the experiments that verify the implementation are briefly presented.
© (2014) COPYRIGHT Society of Photo-Optical Instrumentation Engineers (SPIE). Downloading of the abstract is permitted for personal use only.
Łukasz Godlewski, Łukasz Godlewski, Kordula Świętorzecka, Kordula Świętorzecka, Jan Mulawka, Jan Mulawka, "A computer method of finding valuations forcing validity of LC formulae", Proc. SPIE 9290, Photonics Applications in Astronomy, Communications, Industry, and High-Energy Physics Experiments 2014, 92902X (2 December 2014); doi: 10.1117/12.2075115; https://doi.org/10.1117/12.2075115
PROCEEDINGS
10 PAGES


SHARE
RELATED CONTENT

The Elements Of Adaptive Neural Expert Systems
Proceedings of SPIE (March 20 1989)
A Self-Organising Dictionary For Conceptual Structures
Proceedings of SPIE (May 10 1987)
Graph pyramids as models of human problem solving
Proceedings of SPIE (May 20 2004)
Parallelism In Rule-Based Systems
Proceedings of SPIE (March 28 1988)

Back to Top