Ebner, Gabriel Herbrand constructivization for automated intuitionistic theorem proving. (English) Zbl 1435.68364 Cerrito, Serenella (ed.) et al., Automated reasoning with analytic tableaux and related methods. 28th international conference, TABLEAUX 2019, London, UK, September 3–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11714, 355-373 (2019). MSC: 68V15 03B20 03B35 PDFBibTeX XMLCite \textit{G. Ebner}, Lect. Notes Comput. Sci. 11714, 355--373 (2019; Zbl 1435.68364) Full Text: DOI
Alonderis, R. A proof-search procedure for intuitionistic propositional logic. (English) Zbl 1302.03034 Arch. Math. Logic 52, No. 7-8, 759-778 (2013). Reviewer: Branislav Boričić (Beograd) MSC: 03B20 03F03 03F07 03F20 PDFBibTeX XMLCite \textit{R. Alonderis}, Arch. Math. Logic 52, No. 7--8, 759--778 (2013; Zbl 1302.03034) Full Text: DOI
Otten, Jens A non-clausal connection calculus. (English) Zbl 1333.03004 Brünnler, Kai (ed.) et al., Automated reasoning with analytic tableaux and related methods. 20th international conference, TABLEAUX 2011, Bern, Switzerland, July 4–8, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22118-7/pbk). Lecture Notes in Computer Science 6793. Lecture Notes in Artificial Intelligence, 226-241 (2011). MSC: 03B35 03B10 PDFBibTeX XMLCite \textit{J. Otten}, Lect. Notes Comput. Sci. 6793, 226--241 (2011; Zbl 1333.03004) Full Text: DOI
Otten, Jens Clausal connection-based theorem proving in intuitionistic first-order logic. (English) Zbl 1142.03331 Beckert, Bernhard (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2005, Koblenz, Germany, September 14–17, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28931-3/pbk). Lecture Notes in Computer Science 3702. Lecture Notes in Artificial Intelligence, 245-261 (2005). MSC: 03B35 03B20 PDFBibTeX XMLCite \textit{J. Otten}, Lect. Notes Comput. Sci. 3702, 245--261 (2005; Zbl 1142.03331) Full Text: DOI