Abstract
This paper generalises the tree-based data structure of Δ-tree to be applied to signed propositional formulas. The Δ-trees allow a compact representation for signed formulas as well as for a number of reduction strategies in order to consider only those occurrences of literals which are relevant for the satisfiability of the input formula. The conversions from signed formulas to Δ- trees and vice versa are described and a notion of restricted form based on this representation is introduced, allowing for a compact representation of formulas in order to consider only those occurrences of literals which are relevant for its satisfiability.
Citation
Please, cite this work as:
[GOA99] I. P. de Guzmán, M. Ojeda-Aciego, and Agust'. “Multiple-Valued Tableaux with delta-reductions”. In: Proceedings of the International Conference on Artificial Intelligence, IC-AI ’99, June 28 - July 1, 1999, Las Vegas, Nevada, USA, Volume 1. Ed. by H. R. Arabnia. CSREA Press, 1999, pp. 177-183.
@InProceedings{Guzman1999b,
author = {Inman P. {de Guzm{’a}n} and Manuel Ojeda-Aciego and Agust'Valverde},
booktitle = {Proceedings of the International Conference on Artificial Intelligence, {IC-AI} ’99, June 28 - July 1, 1999, Las Vegas, Nevada, USA, Volume 1},
title = {Multiple-Valued Tableaux with delta-reductions},
year = {1999},
editor = {Hamid R. Arabnia},
pages = {177–183},
publisher = {{CSREA} Press},
abstract = {This paper generalises the tree-based data structure of Δ-tree to be applied to signed propositional formulas. The Δ-trees allow a compact representation for signed formulas as well as for a number of reduction strategies in order to consider only those occurrences of literals which are relevant for the satisfiability of the input formula. The conversions from signed formulas to Δ- trees and vice versa are described and a notion of restricted form based on this representation is introduced, allowing for a compact representation of formulas in order to consider only those occurrences of literals which are relevant for its satisfiability.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/icai/GuzmanOV99.bib},
timestamp = {Fri, 26 Mar 2004 13:51:06 +0100},
}