IJCAR 2022 Proceedings of IJCAR 2022: Author Index

IJCAR 2022 PROCEEDINGS OF IJCAR 2022: AUTHOR INDEX

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