Eliminating definitions and Skolem functions in first-order logic

DOI10.1145/772062.772068zbMath1365.03038OpenAlexW2152535604MaRDI QIDQ5267436

Jeremy Avigad

Publication date: 13 June 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://figshare.com/articles/journal_contribution/Eliminating_Definitions_and_Skolem_Functions_in_First-Order_Logic/6491492

zbMATH Keywords

Skolem functionsproof complexitydefinitionslengths of proofs

Mathematics Subject Classification ID

Classical first-order logic (03B10) First-order arithmetic and fragments (03F30) Complexity of proofs (03F20)

Related Items (9)

Effective Interpolation and Preservation in Guarded Logics ⋮ On the complexity of proof deskolemization ⋮ Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \) ⋮ Finitely axiomatized theories lack self‐comprehension ⋮ Constructive forcing, CPS translations and witness extraction in Interactive realizability ⋮ The price of query rewriting in ontology-based data access ⋮ Non-elementary speed-ups in logic calculi ⋮ The complexity of higher-order queries ⋮ Forcing in Proof Theory

This page was built for publication: Eliminating definitions and Skolem functions in first-order logic