The Challenge of Unifying Semantic and Syntactic Inference Restrictions

Weidenbach, Christoph

doi:10.4204/EPTCS.311.1

Item

ITEM ACTIONSEXPORT

Add to Basket

Please note that a newer version of this item is available:
https://pure.mpg.de/pubman/item/item_3188468_5

DetailsSummary

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 Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

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: https://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.