publikationen

2026

  1. Conf./WS
    Building Blocks for Reasoning on the BEAM
    Johannes Schuster and Christoph Benzmüller
    In 16th International Workshop on the Implementation of Logics (IWIL 2026), October 25, 2026, Spetses, Greece, Oct 2026
    accepted, forthcoming
    PDF
  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
    PDF
  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 Code
  4. Software
    Shot
    Johannes Schuster
    Zenodo, Sep 2026
    Concurrent tableau prover for higher-order logic on the BEAM, released as four packages: shot_ds 1.3.2 (data structures, TH0/TH1 parser, doi:10.5281/zenodo.23044591), shot_un 0.2.2 (pre-unification, pattern unification, second-order matching, doi:10.5281/zenodo.23044593), shot_to 0.2.1 (term order NCPO-LNF, doi:10.5281/zenodo.23044598), shot_tx 0.1.1 (tableau calculus and architecture, doi:10.5281/zenodo.23044601)
    DOI Code
  5. Software
    AtpClient
    Johannes Schuster, Christoph Benzmüller, and David Fuenmayor
    Version 0.6.2, Zenodo, Aug 2026
    Elixir library for uniform access to automated theorem provers via SystemOnTPTP, StarExec, Isabelle and local executables
    DOI Code
  6. Software
    tptp
    Johannes Schuster
    Version 0.1.2, Zenodo, Sep 2026
    Parser, linter and printer for the TPTP language in Elixir, generated from the official syntax BNF
    DOI Code
  7. Software
    AtpMcp
    Johannes Schuster
    Version 0.5.2, Zenodo, Sep 2026
    MCP server that exposes the prover backends of AtpClient to language-model agents via the Model Context Protocol
    DOI Code
  8. Software
    KinoAtpClient
    Johannes Schuster
    Zenodo, 2026
    Livebook (Kino) integration of AtpClient for interactive proving in notebooks
    DOI Code