A note on assumptions about Skolem functions

DOI10.1007/BF00881919zbMath0879.03006OpenAlexW1972410746MaRDI QIDQ1904405

Christoph Weidenbach, Hans Jürgen Ohlbach

Publication date: 20 December 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00881919

zbMATH Keywords

first-order logicpreservation of satisfiabilityrefutational automated theorem-provingsharpened Skolem theoremskolemization

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Related Items (4)

SPASS & FLOTTER version 0.42 ⋮ On the practical value of different definitional translations to normal form ⋮ Practically useful variants of definitional translations to normal form ⋮ Deciding the guarded fragments by resolution

Uses Software

• OTTER
• FLOTTER

Cites Work

• Seventy-five problems for testing automatic theorem provers
• Computational aspects of an order-sorted logic with term declarations
• Semantics-Based Translation Methods for Modal Logics
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A note on assumptions about Skolem functions