Homogeneous Linear Diophantine Equations. - Florian Messner; Julian Parsert; Jonas Schöpf; Christian Sternagel (Arch. Formal Proofs, 2017)

A Formally Verified Solver for Homogeneous Linear Diophantine Equations. - Florian Meßner; Julian Parsert; Jonas Schöpf; Christian Sternagel (ITP, 2018)

TTT2 with Termination Templates for Teaching. - Jonas Schöpf; Christian Sternagel (CoRR, 2018)

Certifying the Weighted Path Order (Invited Talk). - René Thiemann; Jonas Schöpf; Christian Sternagel; Akihisa Yamada 002 (FSCD, 2020)

Confluence Criteria for Logically Constrained Rewrite Systems. - Jonas Schöpf; Aart Middeldorp (CADE, 2023)

Confluence Criteria for Logically Constrained Rewrite Systems (Full Version). - Jonas Schöpf; Aart Middeldorp (CoRR, 2023)

Equational Theories and Validity for Logically Constrained Term Rewriting. - Takahito Aoto 001; Naoki Nishida 001; Jonas Schöpf (FSCD, 2024)

Confluence of Logically Constrained Rewrite Systems Revisited. - Jonas Schöpf; Fabian Mitterwallner; Aart Middeldorp (IJCAR (2), 2024)

Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version). - Takahito Aoto 001; Naoki Nishida 001; Jonas Schöpf (CoRR, 2024)

Automated Analysis of Logically Constrained Rewrite Systems using crest. - Jonas Schöpf; Aart Middeldorp (TACAS (1), 2025)

Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version). - Kanta Takahata; Jonas Schöpf; Naoki Nishida 001; Takahito Aoto 001 (CoRR, 2025)

Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version). - Kanta Takahata; Jonas Schöpf; Naoki Nishida 001; Takahito Aoto 001 (CoRR, 2025)