English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

The Challenge of Unifying Semantic and Syntactic Inference Restrictions

MPS-Authors
/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)

arXiv:1912.12966.pdf
(Preprint), 135KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Weidenbach, C. (2019). The Challenge of Unifying Semantic and Syntactic Inference Restrictions. Electronic Proceedings in Theoretical Computer Science, 311, 5-10. doi:10.4204/EPTCS.311.1.


Cite as: http://hdl.handle.net/21.11116/0000-0005-8750-8
Abstract
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.