On Resolution with Clauses of Bounded Size

DOI10.1137/0206031MaRDI QIDQ4144819zbMATH OpenOpenAlexFDO

Authors Zvi Galil

Publication date 1977

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1137/0206031

Mathematics Subject Classification ID

Classical propositional logic (03B05) Analysis of algorithms and problem complexity (68Q25)

Cited in

(7)

• Seventy-five problems for testing automatic theorem provers
• Typical case complexity of satisfiability algorithms and the threshold phenomenon
• Towards an optimal separation of space and length in resolution
• A bound on the length of a random derivation-search tree in general multi-premise calculi
• Narrow proofs may be maximally long
• Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas
• Learnability with PAC semantics for multi-agent beliefs

This page was built for publication: On Resolution with Clauses of Bounded Size

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