+++
title = "First possible solution: Quantifiers"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5h"]
forwardlinks = ["3a8g5h2"]
zettelid = "3a8g5h1"
+++

The first solution to this problem would be to add quantifiers to the
atoms that cannot always be evaluated at the current spot. However, this
would significantly increase the complexity of the Sat solver, as well
as make predicates unevaluatable in general, because it might contain
quantifiers that don't evaluate to one specific value.

However, with a suitably strong SAT solver, it should be possible to
show the independence between the different predicates. However, the
correctness property should probably be correct as well and should be
checkable with the SAT solver.