scientific article; zbMATH DE number 4037813

MaRDI QIDQ3777987zbMATH OpenFDO

Authors Nail Zamov

Publication date 1987

zbMATH Keywords

first-order proof systemsresolution without Skolemization

Mathematics Subject Classification ID

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

Recommendations

• Translation of resolution proofs into short first-order proofs without choice axioms.
• Translation of resolution proofs into short first-order proofs without choice axioms
• scientific article; zbMATH DE number 510785
• scientific article; zbMATH DE number 627412
• Skolemization in unranked logics

Cited in

(12)

• Complexity of resolution proofs and function introduction
• Resolution calculus for the first order linear logic
• A note on assumptions about Skolem functions
• Translation of resolution proofs into short first-order proofs without choice axioms
• Skolemization modulo theories
• Skolemization in unranked logics
• scientific article; zbMATH DE number 3970135 (Why is no real title available?)
• scientific article; zbMATH DE number 4106803 (Why is no real title available?)
• scientific article; zbMATH DE number 871438 (Why is no real title available?)
• Efficient Skolemization
• Translation of resolution proofs into short first-order proofs without choice axioms.
• Un-Skolemizing clause sets

This page was built for publication:

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