Torán, Jacobo; Wörz, Florian Number of variables for graph differentiation and the resolution of graph isomorphism formulas. (English) Zbl 07713584 ACM Trans. Comput. Log. 24, No. 3, Paper No. 23, 25 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{J. Torán} and \textit{F. Wörz}, ACM Trans. Comput. Log. 24, No. 3, Paper No. 23, 25 p. (2023; Zbl 07713584) Full Text: DOI
Atserias, Albert; Lauria, Massimo; Nordström, Jakob Narrow proofs may be maximally long. (English) Zbl 1367.03104 ACM Trans. Comput. Log. 17, No. 3, Article No. 19, 30 p. (2016). MSC: 03F20 PDFBibTeX XMLCite \textit{A. Atserias} et al., ACM Trans. Comput. Log. 17, No. 3, Article No. 19, 30 p. (2016; Zbl 1367.03104) Full Text: DOI arXiv
Nordström, Jakob; Håstad, Johan Towards an optimal separation of space and length in resolution. (English) Zbl 1366.68098 Theory Comput. 9, Paper No. 14, 471-557 (2013). MSC: 68Q25 03F20 68Q15 68Q17 68T15 PDFBibTeX XMLCite \textit{J. Nordström} and \textit{J. Håstad}, Theory Comput. 9, Paper No. 14, 471--557 (2013; Zbl 1366.68098) Full Text: DOI
Franco, John Typical case complexity of satisfiability algorithms and the threshold phenomenon. (English) Zbl 1101.68838 Discrete Appl. Math. 153, No. 1-3, 89-123 (2005). MSC: 68T20 68W05 68Q25 PDFBibTeX XMLCite \textit{J. Franco}, Discrete Appl. Math. 153, No. 1--3, 89--123 (2005; Zbl 1101.68838) Full Text: DOI
Kur’erov, Yu. N. A bound on the length of a random derivation-search tree in general multi-premise calculi. (English. Russian original) Zbl 0752.03022 Cybernetics 27, No. 3, 462-466 (1991); translation from Kibernetika 1991, No. 3, 112-115 (1991). MSC: 03D15 PDFBibTeX XMLCite \textit{Yu. N. Kur'erov}, Cybernetics 27, No. 3, 462--466 (1991; Zbl 0752.03022); translation from Kibernetika 1991, No. 3, 112--115 (1991) Full Text: DOI
Pelletier, Francis Jeffry Seventy-five problems for testing automatic theorem provers. (English) Zbl 0642.68147 J. Autom. Reasoning 2, 191-216 (1986). MSC: 68T15 PDFBibTeX XMLCite \textit{F. J. Pelletier}, J. Autom. Reasoning 2, 191--216 (1986; Zbl 0642.68147) Full Text: DOI