Skip to Main content Skip to Navigation
Conference papers

The Challenge of Unifying Semantic and Syntactic Inference Restrictions

Christoph Weidenbach 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-02406673
Contributor : Stephan Merz <>
Submitted on : Thursday, December 12, 2019 - 11:06:46 AM
Last modification on : Tuesday, December 17, 2019 - 2:25:12 AM
Long-term archiving on: : Friday, March 13, 2020 - 7:40:55 PM

File

arcade19.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02406673, version 1

Collections

Citation

Christoph Weidenbach. The Challenge of Unifying Semantic and Syntactic Inference Restrictions. 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019), 2019, Natal, Brazil. ⟨hal-02406673⟩

Share

Metrics

Record views

46

Files downloads

84