A note on assumptions about Skolem functions

DOI10.1007/BF00881919zbMATH Open0879.03006OpenAlexW1972410746MaRDI QIDQ1904405FDOQ1904405

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computational aspects of an order-sorted logic with term declarations
• Seventy-five problems for testing automatic theorem provers
• Semantics-Based Translation Methods for Modal Logics

Cited In (6)

• Title not available (Why is that?)
• On the practical value of different definitional translations to normal form
• SPASS & FLOTTER version 0.42
• Practically useful variants of definitional translations to normal form
• Title not available (Why is that?)
• Deciding the guarded fragments by resolution

Uses Software

• OTTER
• FLOTTER

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

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