Eliminating definitions and Skolem functions in first-order logic

DOI10.1145/772062.772068zbMATH Open1365.03038OpenAlexW2152535604MaRDI QIDQ5267436FDOQ5267436

Authors: 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

Recommendations

• On Skolem functions in proof theory
• A note on definable Skolem functions
• scientific article; zbMATH DE number 627412
• Elimination of Skolem functions for monotone formulas in analysis
• A note on assumptions about Skolem functions

zbMATH Keywords

proof complexitySkolem functionsdefinitionslengths of proofs

Mathematics Subject Classification ID

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

Cited In (13)

• First-order atom definitions extended
• A unifying principle for clause elimination in first-order logic
• The price of query rewriting in ontology-based data access
• Constructive forcing, CPS translations and witness extraction in Interactive realizability
• Finitely axiomatized theories lack self‐comprehension
• Skolem functions of arithmetical sentences.
• Elimination Theorems of Uniqueness Conditions
• Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
• Non-elementary speed-ups in logic calculi
• Forcing in Proof Theory
• Effective Interpolation and Preservation in Guarded Logics
• On the complexity of proof deskolemization
• The complexity of higher-order queries

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5267436)