Talk Author Index

TALK AUTHOR INDEX

Shortcuts: A B C D E F G H I J K L M N O P Q R S T U V W Y Z

A
Akshay, S.	On eventual non-negativity and positivity for the weighted sum of powers of matrices
Albert, Elvira	Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Alrabbaa, Christian	Evonne: Interactive Proof Visualization for Description Logics (System Description)
B
Baader, Franz	Evonne: Interactive Proof Visualization for Description Logics (System Description)
Barbosa, Haniel	Flexible Proof Production in an Industrial-Strength SMT Solver
Barrett, Clark	Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) Reasoning About Vectors using an SMT Theory of Sequences Flexible Proof Production in an Industrial-Strength SMT Solver
Berg, Jeremias	Clause Redundancy and Preprocessing in Maximum Satisfiability
Bernreiter, Michael	Sequent Calculi for Choice Logics
Bidoit, Nicole	Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications
Bilkova, Marta	Paraconsistent Gödel modal logic
Blaisdell, Eben	Non-associative, non-commutative multi-modal linear logic
Borgwardt, Stefan	Evonne: Interactive Proof Visualization for Description Logics (System Description)
Bouziane, Hinde	Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Bozga, Marius	Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
Bromberger, Martin	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Brown, Chad	Lash 1.0 (System Description)
Bryant, Randal	Preprocessing of Propagation Redundant Clauses
Bueri, Lucas	Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
C
Cailler, Julie	Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Cauli, Claudia	Actions over Core-closed Knowledge Bases
Chakraborty, Supratik	On eventual non-negativity and positivity for the weighted sum of powers of matrices
Chlebowski, Szymon	Synthetic tableaux: minimal tableau search heuristics
D
Dachselt, Raimund	Evonne: Interactive Proof Visualization for Description Logics (System Description)
Das, Anupam	Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Delahaye, David	Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Dill, David	Reasoning About Vectors using an SMT Theory of Sequences
Dixon, Clare	Local Reductions for the Modal Cube
Dowek, Gilles	From the Universality of Mathematical Truth to the Interoperability of Proof Systems (Invited Talk)
Draheim, Dirk	GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Duarte, André	Ground joinability and connectedness in the superposition calculus
Durán, Francisco	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
E
Eker, Steven	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Escobar, Santiago	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
F
Felli, Paolo	CTL* model checking for data-aware dynamic systems with arithmetic
Ferrari, Mauro	SAT-based Proof Search in Intermediate Propositional Logics
Fiorentini, Camillo	SAT-based Proof Search in Intermediate Propositional Logics
Frittella, Sabine	Paraconsistent Gödel modal logic
Frohn, Florian	Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Fujita, Tomohiro	Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)
G
Gallicchio, James	Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Giesl, Jürgen	Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Girlando, Marianna	Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Gordillo, Pablo	Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Grieskamp, Wolfgang	Reasoning About Vectors using an SMT Theory of Sequences
H
Haifani, Fajar	Connection-minimal Abduction in EL via translation to FOL Semantic Relevance
Hernández-Cerezo, Alejandro	Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Heskes, Tom	Guiding an Automated Theorem Prover with Neural Rewriting
Heule, Marijn	Preprocessing of Propagation Redundant Clauses
Holden, Sean	Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Holub, Štěpán	Binary codes that do not preserve primitivity
Hustadt, Ullrich	Local Reductions for the Modal Cube
I
Ihalainen, Hannes	Clause Redundancy and Preprocessing in Maximum Satisfiability
Indrzejczak, Andrzej	Le\'sniewski's Ontology -- Proof-Theoretic Characterization
Iosif, Radu	Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
J
Janota, Mikolas	Guiding an Automated Theorem Prover with Neural Rewriting
Jukiewicz, Marcin	Synthetic tableaux: minimal tableau search heuristics
Järv, Priit	GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Järvisalo, Matti	Clause Redundancy and Preprocessing in Maximum Satisfiability
K
Kaliszyk, Cezary	Lash 1.0 (System Description)
Kanovich, Max	Non-associative, non-commutative multi-modal linear logic
Koopmann, Patrick	Connection-minimal Abduction in EL via translation to FOL Evonne: Interactive Proof Visualization for Description Logics (System Description)
Korovin, Konstantin	Ground joinability and connectedness in the superposition calculus
Kozhemiachenko, Daniil	Paraconsistent Gödel modal logic
Kremer, Gereon	Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) Flexible Proof Production in an Industrial-Strength SMT Solver
Kutsia, Temur	A framework for approximate generalization in quantitative theories (ONLINE)
Kuznetsov, Stepan	Non-associative, non-commutative multi-modal linear logic
L
Lachnitt, Hanna	Flexible Proof Production in an Industrial-Strength SMT Solver
Lahav, Ori	Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices
Larry, Paulson	Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Leidinger, Hendrik	SCL(EQ): SCL for First-Order Logic with Equality
Leszczyńska-Jasion, Dorota	Synthetic tableaux: minimal tableau search heuristics
Leutgeb, Lorenz	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Lolic, Anela	Sequent Calculi for Choice Logics
Lommen, Nils	Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
M
Ma, Yue	Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications
Maly, Jan	Sequent Calculi for Choice Logics
Mangla, Chaitanya	Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Marcos, Joao	Finite two-dimensional proof systems for non-finitely axiomatizable logics
Marti-Oliet, Narciso	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Matsuzaki, Takuya	Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)
Meseguer, Jose	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Meyer, Fabian	Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Mitsch, Stefan	Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Montali, Marco	CTL* model checking for data-aware dynamic systems with arithmetic
Méndez, Julián	Evonne: Interactive Proof Visualization for Description Logics (System Description)
N
Nalon, Cláudia	Local Reductions for the Modal Cube
Niemetz, Aina	Flexible Proof Production in an Industrial-Strength SMT Solver
Noetzli, Andres	Reasoning About Vectors using an SMT Theory of Sequences Flexible Proof Production in an Industrial-Strength SMT Solver
O
Ortiz, Magdalena	Actions over Core-closed Knowledge Bases
Ozdemir, Alex	Flexible Proof Production in an Industrial-Strength SMT Solver
P
Pal, Debtanu	On eventual non-negativity and positivity for the weighted sum of powers of matrices
Papacchini, Fabio	Local Reductions for the Modal Cube
Park, Junkil	Reasoning About Vectors using an SMT Theory of Sequences
Pau, Cleo	A framework for approximate generalization in quantitative theories (ONLINE)
Piepenbrock, Jelle	Guiding an Automated Theorem Prover with Neural Rewriting
Pimentel, Elaine	Non-associative, non-commutative multi-modal linear logic
Piterman, Nir	Actions over Core-closed Knowledge Bases
Platzer, André	Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Popescu, Andrei	Rensets and Renaming-Based Recursion for Syntax and Bindings
Preiner, Mathias	Flexible Proof Production in an Industrial-Strength SMT Solver
Q
Qadeer, Shaz	Reasoning About Vectors using an SMT Theory of Sequences
R
Raška, Martin	Binary codes that do not preserve primitivity
Reeves, Joseph	Preprocessing of Propagation Redundant Clauses
Reynolds, Andrew	Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) Reasoning About Vectors using an SMT Theory of Sequences Flexible Proof Production in an Industrial-Strength SMT Solver
Robillard, Simon	Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Rodrigues Greati, Vitor	Finite two-dimensional proof systems for non-finitely axiomatizable logics
Rodríguez-Núñez, Clara	Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Rosain, Johann	Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)
Rubio, Albert	Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Rubio, Ruben	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
S
Scedrov, Andre	Non-associative, non-commutative multi-modal linear logic
Shankar, Natarajan	The Pleasures of Proof
Sheng, Ying	Reasoning About Vectors using an SMT Theory of Sequences
Sochański, Michał	Synthetic tableaux: minimal tableau search heuristics
Starosta, Štěpán	Binary codes that do not preserve primitivity
Suda, Martin	Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)
T
Talcott, Carolyn	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Tammet, Tanel	GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Tan, Yong Kiam	Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Tinelli, Cesare	Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) Reasoning About Vectors using an SMT Theory of Sequences Flexible Proof Production in an Industrial-Strength SMT Solver
Tomczyk, Agata	Synthetic tableaux: minimal tableau search heuristics
Tourret, Sophie	Connection-minimal Abduction in EL via translation to FOL
U
Urban, Josef	Guiding an Automated Theorem Prover with Neural Rewriting
V
Viswanathan, Arjun	Flexible Proof Production in an Industrial-Strength SMT Solver
Viteri, Scott	Flexible Proof Production in an Industrial-Strength SMT Solver
W
Weidenbach, Christoph	Connection-minimal Abduction in EL via translation to FOL SCL(EQ): SCL for First-Order Logic with Equality An Efficient Subsumption Test Pipeline for BS(LRA) Clauses Semantic Relevance
Winkler, Sarah	CTL* model checking for data-aware dynamic systems with arithmetic
Woltran, Stefan	Sequent Calculi for Choice Logics
Y
Yamada, Akihisa	Term Ordering for Non-Reachability of (Conditional) Rewriting
Yang, Hui	Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications
Z
Zohar, Yoni	Reasoning About Vectors using an SMT Theory of Sequences Flexible Proof Production in an Industrial-Strength SMT Solver Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices