Eliminating definitions and Skolem functions in first-order logic

DOI10.1145/772062.772068MaRDI QIDQ5267436zbMATHOpenAlexFDO

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

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)

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

Cited in

(15)

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

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)