Christoph Weidenbach (Max Planck Institute for Informatics) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.311.1 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |