KIAM Main page Web Library  •  Publication Searh  Русский 
Publication

Article collection "Mathematical Problems of Cybernetics" №15, Moscow, 2006
Authors: Khelemendik R. V.
An algorithm for determining satisfiability formulae of computation tree logic and an effective algorithm for constructing inferences of valid formulas from axioms
Abstract:
Discusses the computation tree logic (CTL) which is a generalization of propositional logic by introducing special temporal operators and the quantifiers in front of them. The truth of formulas is defined by the values of propositional variables at the vertices of a connected directed graph. In this paper an original tabular algorithm for determining satisfiability formulae of CTL and building a model for satisfiable one was constructed and described in details. The detailed proof of soundness and completeness of this algorithm was presented. An effective algorithm for constructing inferences of valid formulas from axioms was formulated, and it's completeness and soundness were proved.
Keywords:
computation tree logic, satisfiability, validity, algorithm, model, axiom, logic inference
Publication language: russian,  pages: 60 (p. 217-266)
Research direction:
Mathematical problems and theory of numerical methods
Russian source text:
List of publications citation:
Export link to publication in format:   RIS    BibTeX
About authors:
  • Khelemendik Roman Viktorovich,  orcid.org/0000-0002-5244-6456KIAM RAS