Bases for closed sets of implicants and implicates in temporal logic |
| |
Authors: | P Cordero M Enciso IP de Guzmán |
| |
Affiliation: | (1) E.T.S.I. Informática, Universidad de Málaga, Campus de Teatinos, 29071 Málaga, Spain (e-mail: pcordero@uma.es, enciso@lcc.uma.es, guzman@ctima.uma.es) , ES |
| |
Abstract: | Prime implicates and implicants are used in several areas of Artificial Intelligence. However, their calculation is not always
an easy task. Nevertheless, it is important to remark the distinction between (i) computing the prime implicates and implicants and (ii) using the information they contain.
In this paper, we present a way in which (ii) can be done without actually doing (i) by limiting prime implicants and implicates management to unitary implicants and implicates. Besides, we outline how the
use of this technique is particularly relevant in the field of automated deduction in temporal logics. The information contained
in temporal implicates and implicants can be used to design transformations of temporal formulae able to increase the power
of automated deduction techniques for temporal logics. Particularly, we have developed a theory for unitary temporal implicates and implicants that can be more efficiently computed than prime implicants, while still providing the information needed to design this
kind of transformations.
The theory we have developed in this paper is easily extensible to cover different types of temporal logics, and is integrable
in different automated deduction methods for these temporal logics.
Received: 14 May 1999 / 22 March 2002 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|