IJCAR 2024: INTERNATIONAL JOINT CONFERENCE ON AUTOMATED REASONING

A
Acclavio, Matteo	Sequent Systems on Undirected Graphs
Amrollahi, Daneshvar	Synthesis of Recursive Programs in Saturation
Arrial, Victor	The Benefits of Diligence
Avigad, Jeremy	Automated Reasoning for Mathematics
Ayala-Rincón, Mauricio	Equational Anti-Unification over Absorption Theories
B
Baader, Franz	Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies
Balbiani, Philippe	Local Intuitionistic Modal Logics and Their Calculi
Barrett, Clark	Generalized Optimization Modulo Theories
Berg, Jeremias	Certified MaxSAT Preprocessing
Bhayat, Ahmed	A Higher-Order Vampire
Biere, Armin	Certifying Phase Abstraction
Bonsangue, Marcello	Equivalence Checking of Quantum Circuits by Model Counting
Bozec, Tanguy	What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
Bromberger, Martin	First-Order Automatic Literal Model Generation
Brown, Chad E.	Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Bruni, Alessandro	Skolemization for Intuitionistic Linear Logic
Bártek, Filip	Regularization in Spider-style Strategy Discovery and Schedule Construction
C
Cerna, David	Equational Anti-Unification over Absorption Theories
Chassot, Samuel	Verifying a Realistic Mutable Hash Table: Case Study
Chvalovský, Karel	Regularization in Spider-style Strategy Discovery and Schedule Construction
Ciabattoni, Agata	Sequents vs hypersequents for Aqvist systems
Coopmans, Tim	Equivalence Checking of Quantum Circuits by Model Counting
D
Das, Anupam	A proof theory of (omega) context-free languages, via non-wellfounded proofs
De, Abhishek	A proof theory of (omega) context-free languages, via non-wellfounded proofs
De Lon, Adrian	The Naproche-ZF theorem prover (short paper/system description)
Dixon, Clare	Model Construction for Modal Clauses
E
Ehling, Georg	Solving Quantitative Equations
Einarsdóttir, Sólrún Halla	Lemma Discovery and Strategies for Automated Induction
F
Fernandez Gil, Oliver	Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies
Ferrari, Mauro	A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property
Fiorentini, Camillo	A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property
Frohn, Florian	Satisfiability Modulo Exponential Integer Arithmetic
Froleyks, Nils	Certifying Phase Abstraction
Fruzsa, Krisztina	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
Férée, Hugo	Mechanised uniform interpolation for modal logics K, GL and iSL
G
Gao, Han	Local Intuitionistic Modal Logics and Their Calculi
Garcia, Ronald	A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations
Ge, Rui	A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations
Gencer, Çigdem	Local Intuitionistic Modal Logics and Their Calculi
Ghilardi, Silvio	Model Completeness for Rational Trees
Giesl, Jürgen	Satisfiability Modulo Exponential Integer Arithmetic A Dependency Pair Framework for Relative Termination of Term Rewriting Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
González Barragan, Andrés Felipe	Equational Anti-Unification over Absorption Theories
Graham-Lengrand, Stéphane	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
Guerrieri, Giulio	The Benefits of Diligence
H
Hader, Thomas	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
Hajdu, Márton	Induction in Saturation Reducibility Constraints in Superposition Synthesis of Recursive Programs in Saturation Lemma Discovery and Strategies for Automated Induction
Heisinger, Maximilian	Quantifier Shifting for Quantified Boolean Formulas Revisited Booleguru, the Propositional Polyglot
Heisinger, Simone	Quantifier Shifting for Quantified Boolean Formulas Revisited Booleguru, the Propositional Polyglot
Heljanko, Keijo	Certifying Phase Abstraction
Heuer, Jan	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Hozzová, Petra	Induction in Saturation Synthesis of Recursive Programs in Saturation
Hustadt, Ullrich	Model Construction for Modal Clauses
I
Ihalainen, Hannes	Certified MaxSAT Preprocessing
Irfan, Ahmed	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
J
Johansson, Moa	Lemma Discovery and Strategies for Automated Induction
Järvisalo, Matti	Certified MaxSAT Preprocessing
K
Kaliszyk, Cezary	Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Kassing, Jan-Christoph	A Dependency Pair Framework for Relative Termination of Term Rewriting
Kaufmann, Daniela	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
Kesner, Delia	The Benefits of Diligence
Khalid, Zain	An Empirical Assessment of Progress in Automated Theorem Proving
Kotthoff, Lars	An Empirical Assessment of Progress in Automated Theorem Proving
Kovács, Laura	Induction in Saturation Reducibility Constraints in Superposition MCSat-based Finite Field Reasoning in the Yices2 SMT Solver Synthesis of Recursive Programs in Saturation
Kozen, Dexter	A cyclic proof system for Guarded Kleene Algebra with Tests
Krasnopol, Florent	First-Order Automatic Literal Model Generation
Kunčak, Viktor	Verifying a Realistic Mutable Hash Table: Case Study
Kutsia, Temur	Solving Quantitative Equations Equational Anti-Unification over Absorption Theories
Kuznets, Roman	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
L
Laarman, Alfons	Equivalence Checking of Quantum Circuits by Model Counting
Lammich, Peter	Fast and Verified UNSAT Certificate Checking
Lommen, Nils	Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
M
Mei, Jingyi	Equivalence Checking of Quantum Circuits by Model Counting
Meyer, Eleanore	Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
Middeldorp, Aart	Confluence of Logically Constrained Rewrite Systems Revisited
Mitterwallner, Fabian	Confluence of Logically Constrained Rewrite Systems Revisited
Myreen, Magnus O.	Certified MaxSAT Preprocessing
Möhle, Sibylle	First-Order Automatic Literal Model Generation
N
Nalon, Cláudia	Non-Iterative Modal Resolution Model Construction for Modal Clauses
Niederhauser, Johannes	Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Nordström, Jakob	Certified MaxSAT Preprocessing
O
Oertel, Andy	Certified MaxSAT Preprocessing
Olivetti, Nicola	Local Intuitionistic Modal Logics and Their Calculi
P
Papacchini, Fabio	Model Construction for Modal Clauses
Pattinson, Dirk	Non-Iterative Modal Resolution
Peltier, Nicolas	What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
Perrault, C. Raymond	An Empirical Assessment of Progress in Automated Theorem Proving
Petitjean, Quentin	What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
Platzer, André	Uniform Substitution for Differential Refinement Logic
Poidomani, Lia Maria	Model Completeness for Rational Trees
Pommellet, Adrien	SAT-based Learning of Computation Tree Logic
Prebet, Enguerrand	Uniform Substitution for Differential Refinement Logic
R
Rawson, Michael	Reducibility Constraints in Superposition
Rebola-Pardo, Adrian	Quantifier Shifting for Quantified Boolean Formulas Revisited
Ritter, Eike	Skolemization for Intuitionistic Linear Logic
Rooduijn, Jan	A cyclic proof system for Guarded Kleene Algebra with Tests
Ruess, Harald	A Decision Method for First-Order Stream Logic
S
Scatton, Simon	SAT-based Learning of Computation Tree Logic
Schmid, Ulrich	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
Schuermann, Carsten	Skolemization for Intuitionistic Linear Logic
Schöpf, Jonas	Confluence of Logically Constrained Rewrite Systems Revisited
Seidl, Martina	Quantifier Shifting for Quantified Boolean Formulas Revisited Booleguru, the Propositional Polyglot
Shillito, Ian	Mechanised uniform interpolation for modal logics K, GL and iSL
Sighireanu, Mihaela	What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
Silva, Alexandra	A cyclic proof system for Guarded Kleene Algebra with Tests
Smallbone, Nicholas	Lemma Discovery and Strategies for Automated Induction
Stan, Daniel	SAT-based Learning of Computation Tree Logic
Suda, Martin	Regularization in Spider-style Strategy Discovery and Schedule Construction A Higher-Order Vampire Lemma Discovery and Strategies for Automated Induction
Summers, Alexander J.	A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations
Sutcliffe, Geoff	Stepping Stones in the TPTP World An Empirical Assessment of Progress in Automated Theorem Proving
Suttner, Christian	An Empirical Assessment of Progress in Automated Theorem Proving
T
Tan, Yong Kiam	Certified MaxSAT Preprocessing
Tesi, Matteo	Sequents vs hypersequents for Aqvist systems
Tinelli, Cesare	Generalized Optimization Modulo Theories
Tsiskaridze, Nestan	Generalized Optimization Modulo Theories
V
van der Giessen, Iris	Mechanised uniform interpolation for modal logics K, GL and iSL
van Ditmarsch, Hans	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
van Gool, Sam	Mechanised uniform interpolation for modal logics K, GL and iSL
Vartanyan, Grigory	A Dependency Pair Framework for Relative Termination of Term Rewriting
Voronkov, Andrei	Induction in Saturation Reducibility Constraints in Superposition Synthesis of Recursive Programs in Saturation
W
Wagner, Eva Maria	Synthesis of Recursive Programs in Saturation
Waldmann, Uwe	On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus
Weidenbach, Christoph	First-Order Automatic Literal Model Generation
Wernhard, Christoph	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Y
Yu, Emily	Certifying Phase Abstraction

Disclaimer | Powered by EasyChair Smart Program