The Challenge of Unifying Semantic and Syntactic Inference Restrictions

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.

In Martin Suda and Sarah Winkler: Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019), Natal, Brazil, August 26, 2019, Electronic Proceedings in Theoretical Computer Science 311, pp. 5–10.
Published: 31st December 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.311.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org