Checking the Satisfiability of Formulas Represented in Disjunctive Normal Form in the Language <Emphasis Type="Italic">L.</Emphasis> I |
| |
Authors: | S L Kryvyj A N Chebotarev |
| |
Affiliation: | (1) Cybernetics Institute, National Academy of Sciences of Ukraine, Kiev, Ukraine |
| |
Abstract: | An original technique is proposed for checking the satisfiability of formulae represented in the logical language L in the
form of a set of conjuncts. Satisfiability checking is performed by means of analysis and transformation of some relations
defined over the set of conjuncts.
__________
Translated from Kibernetika i Sistemnyi Analiz, No. 4, pp. 22–28, July–August 2005. |
| |
Keywords: | reactive algorithms specification language L formula satisfiability depth of a formula set of conjuncts |
本文献已被 SpringerLink 等数据库收录! |