TY - GEN
T1 - Subsumption algorithms for three-valued geometric resolution
AU - de Nivelle, Hans
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - In an implementation of geometric resolution, the most costly operation is subsumption (or matching): One has to decide for a three-valued, geometric formula, whether this formula is false in a given interpretation. The formula contains only atoms with variables, equality, and existential quantifiers. The interpretation contains only atoms with constants. Because the atoms have no term structure, matching for geometric resolution is a hard problem. We translate the matching problem into a generalized constraint satisfaction problem, and give an algorithm that solves it efficiently. The algorithm uses learning techniques, similar to clause learning in propositional logic. Secondly, we adapt the algorithm in such a way that it finds solutions that use a minimal subset of the interpretation. The techniques presented in this paper may have applications in constraint solving.
AB - In an implementation of geometric resolution, the most costly operation is subsumption (or matching): One has to decide for a three-valued, geometric formula, whether this formula is false in a given interpretation. The formula contains only atoms with variables, equality, and existential quantifiers. The interpretation contains only atoms with constants. Because the atoms have no term structure, matching for geometric resolution is a hard problem. We translate the matching problem into a generalized constraint satisfaction problem, and give an algorithm that solves it efficiently. The algorithm uses learning techniques, similar to clause learning in propositional logic. Secondly, we adapt the algorithm in such a way that it finds solutions that use a minimal subset of the interpretation. The techniques presented in this paper may have applications in constraint solving.
UR - https://www.scopus.com/pages/publications/84976604883
UR - https://www.scopus.com/pages/publications/84976604883#tab=citedBy
U2 - 10.1007/978-3-319-40229-1_18
DO - 10.1007/978-3-319-40229-1_18
M3 - Conference contribution
AN - SCOPUS:84976604883
SN - 9783319402284
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 257
EP - 272
BT - Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings
A2 - Olivetti, Nicola
A2 - Tiwari, Ashish
PB - Springer Verlag
T2 - 8th International Joint Conference on Automated Reasoning, IJCAR 2016
Y2 - 27 June 2016 through 2 July 2016
ER -