Datensatz

Zusammenfassung

While syntactic inference restrictions don't play an important role for SAT,
they are an essential reasoning technique for more expressive logics, such as
first-order logic, or fragments thereof. In particular, they can result in
short proofs or model representations. On the other hand, semantically guided
inference systems enjoy important properties, such as the generation of solely
non-redundant clauses. I discuss to what extend the two paradigms may be
unifiable.