Un-Skolemizing clause sets

DOI10.1016/0020-0190(88)90119-6zbMath0709.03007OpenAlexW2085711600MaRDI QIDQ920968

William W. McCune

Publication date: 1988

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(88)90119-6

zbMATH Keywords

algorithmquantificationsatisfiabilityclauses

Mathematics Subject Classification ID

Related Items (3)

On the strength and scope of DLS ⋮ Constructing specification morphisms ⋮ On the mechanical derivation of loop invariants

Cites Work

• Unnamed Item
• A complete, nonredundant algorithm for reversed Skolemization
• Schubert's steamroller problem: Formulations and solutions
• Extracting information from resolution proof trees
• Maintaining state constraints in relational databases: a proof theoretic basis

This page was built for publication: Un-Skolemizing clause sets