publications

2026

1. Conf./WS

   Building Blocks for Reasoning on the BEAM

   Johannes Schuster and Christoph Benzmüller

   In Proceedings of the 16th International Workshop on the Implementation on Logics (IWIL 2026) and the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-26, short papers), Spetses, Greece, Oct 2026

   DOI Bib PDF Slides

   @inproceedings{schuster2026buildingblocks,
     author = {Schuster, Johannes and Benzmüller, Christoph},
     title = {Building Blocks for Reasoning on the {BEAM}},
     booktitle = {Proceedings of the 16th International Workshop on the Implementation on Logics ({IWIL} 2026) and the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning ({LPAR}-26, short papers), Spetses, Greece},
     editor = {Schulz, Stephan and Korovin, Konstantin and Rawson, Michael},
     series = {Kalpa Publications in Computing},
     volume = {23},
     pages = {98--111},
     publisher = {EasyChair},
     year = {2026},
     month = oct,
     doi = {10.29007/z6j1},
     url = {https://easychair.org/publications/paper/SDCR},
   }

2. Conf./WS

   Elixir meets TPTP: Bringing Automated Reasoning to the BEAM Ecosystem

   Johannes Schuster, David Fuenmayor, and Christoph Benzmüller

   In Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR 2026), co-located with FLoC 2026, Lisbon, Portugal, July 25, 2026, 2026

   Bib PDF

   @inproceedings{schuster2026elixirmeetstptp,
     author = {Schuster, Johannes and Fuenmayor, David and Benzmüller, Christoph},
     title = {{Elixir} meets {TPTP}: Bringing Automated Reasoning to the {BEAM} Ecosystem},
     booktitle = {Proceedings of the Workshop on Practical Aspects of Automated Reasoning ({PAAR} 2026), co-located with {FLoC} 2026, Lisbon, Portugal, July 25, 2026},
     editor = {Hajdu, Márton and Nalon, Cláudia and Suda, Martin},
     series = {CEUR Workshop Proceedings},
     volume = {4241},
     publisher = {CEUR-WS.org},
     year = {2026},
     url = {https://ceur-ws.org/Vol-4241/},
   }

3. Thesis

   Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

   Johannes Schuster

   Otto-Friedrich-Universität Bamberg, 2026

   Executable Livebook notebooks and typeset version

   DOI Bib PDF Livebooks

   @mastersthesis{schuster2026thesis,
     author = {Schuster, Johannes},
     title = {Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving},
     school = {Otto-Friedrich-Universität Bamberg},
     year = {2026},
     doi = {10.5281/zenodo.22045933},
     note = {Executable Livebook notebooks and typeset version},
   }

4. Software

   Shot

   Johannes Schuster

   Zenodo, Sep 2026

   Concurrent tableau prover for higher-order logic on the BEAM, released as four packages: shot_ds (data structures, TH0/TH1 parser, doi:10.5281/zenodo.23044590), shot_un (pre-unification, pattern unification, second-order matching, doi:10.5281/zenodo.23044592), shot_to (term order NCPO-LNF, doi:10.5281/zenodo.23044597), shot_tx (tableau calculus and architecture, doi:10.5281/zenodo.23044599)

   DOI Bib Code shot_ds docs shot_un docs shot_to docs shot_tx docs

   @misc{schuster2026shot,
     author = {Schuster, Johannes},
     title = {Shot},
     publisher = {Zenodo},
     year = {2026},
     month = sep,
     doi = {10.5281/zenodo.23044599},
     note = {Concurrent tableau prover for higher-order logic on the BEAM, released as four packages: shot_ds (data structures, TH0/TH1 parser, doi:10.5281/zenodo.23044590), shot_un (pre-unification, pattern unification, second-order matching, doi:10.5281/zenodo.23044592), shot_to (term order NCPO-LNF, doi:10.5281/zenodo.23044597), shot_tx (tableau calculus and architecture, doi:10.5281/zenodo.23044599)},
   }

5. Software

   AtpClient

   Johannes Schuster, Christoph Benzmüller, and David Fuenmayor

   Zenodo, Aug 2026

   Elixir library for uniform access to automated theorem provers via SystemOnTPTP, StarExec, Isabelle and local executables

   DOI Bib Code Docs

   @misc{schuster2026atpclient,
     author = {Schuster, Johannes and Benzmüller, Christoph and Fuenmayor, David},
     title = {AtpClient},
     publisher = {Zenodo},
     year = {2026},
     month = aug,
     doi = {10.5281/zenodo.21839441},
     note = {Elixir library for uniform access to automated theorem provers via SystemOnTPTP, StarExec, Isabelle and local executables},
   }

6. Software

   tptp

   Johannes Schuster

   Zenodo, Sep 2026

   Parser, linter and printer for the TPTP language in Elixir, generated from the official syntax BNF

   DOI Bib Code Docs

   @misc{schuster2026tptp,
     author = {Schuster, Johannes},
     title = {tptp},
     publisher = {Zenodo},
     year = {2026},
     month = sep,
     doi = {10.5281/zenodo.23063474},
     note = {Parser, linter and printer for the TPTP language in Elixir, generated from the official syntax BNF},
   }

7. Software

   AtpMcp

   Johannes Schuster

   Zenodo, Sep 2026

   MCP server that exposes the prover backends of AtpClient to language-model agents via the Model Context Protocol

   DOI Bib Code Docs

   @misc{schuster2026atpmcp,
     author = {Schuster, Johannes},
     title = {AtpMcp},
     publisher = {Zenodo},
     year = {2026},
     month = sep,
     doi = {10.5281/zenodo.23044594},
     note = {MCP server that exposes the prover backends of AtpClient to language-model agents via the Model Context Protocol},
   }

8. Software

   KinoAtpClient

   Johannes Schuster

   Zenodo, 2026

   Livebook (Kino) integration of AtpClient for interactive proving in notebooks

   DOI Bib Code Docs

   @misc{schuster2026kinoatpclient,
     author = {Schuster, Johannes},
     title = {KinoAtpClient},
     publisher = {Zenodo},
     year = {2026},
     doi = {10.5281/zenodo.23105110},
     note = {Livebook (Kino) integration of AtpClient for interactive proving in notebooks},
   }