Accepted Papers

Papers accepted at IJCAR 2024

Full papers

  • M. Acclavio. Sequent Systems on Undirected Graphs.
  • D. Amrollahi, M. Hajdu, P. Hozzová, L. Kovács, A. Voronkov, E.M. Wagner. Synthesis of Recursive Programs in Saturation.
  • V. Arrial, G. Guerrieri, D. Kesner. The Benefits of Diligence.
  • F. Baader, O. Fernandez Gil. Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies.
  • Ph. Balbiani, H. Gao, Ç. Gencer, N. Olivetti. Local Intuitionistic Modal Logics and Their Calculi.
  • F. Bártek, K. Chvalovský, M. Suda. Regularization in Spider-style Strategy Discovery and Schedule Construction.
  • T. Bozec, N. Peltier, Q. Petitjean, M. Sighireanu. What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
  • M. Bromberger, F. Krasnopol, S. Möhle, C. Weidenbach. First-Order Automatic Literal Model Generation.
  • A. Bruni, E. Ritter, C. Schuermann. Skolemization for Intuitionistic Linear Logic.
  • D. Cerna, M. Ayala-Rincón, T. Kutsia, A.F. González Barragan. Equational Anti-Unification over Absorption Theories.
  • A. Ciabattoni, M. Tesi. Sequents vs hypersequents for Aqvist systems.
  • A. Das, A. De. A proof theory of (omega) context-free languages, via non-wellfounded proofs.
  • H. van Ditmarsch, K. Fruzsa, R. Kuznets, U. Schmid. A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems.
  • H. Férée, I. van der Giessen, S. van Gool, I. Shillito. Mechanised uniform interpolation for modal logics K, GL and ISL.
  • C. Fiorentini, M. Ferrari. A terminating sequent calculus for Intuitionistic Strong Löb Logic.
  • G. Ehling, T. Kutsia. Solving Quantitative Equations.
  • S.H. Einarsdóttir, M. Hajdu, M. Johansson, N. Smallbone, M. Suda. Lemma Discovery and Strategies for Automated Induction.
  • F. Frohn, J. Giesl. Satisfiability Modulo Exponential Integer Arithmetic.
  • N. Froleyks, E. Yu, A. Biere, K. Heljanko. Certifying Phase Abstraction.
  • R. Ge, R. Garcia, A.J. Summers. A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations.
  • S. Ghilardi, L.M. Poldomani. Model Completeness for Rational Trees.
  • M. Hajdu, L. Kovács, M. Rawson, A. Voronkov. Reducibility Constraints in Superposition.
  • S. Heisinger, M. Heisinger, A. Rebola-Pardo, M. Seidl. Quantifier Shifting for Quantified Boolean Formulas Revisited.
  • J. Heuer, C. Wernhard. Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic.
  • U. Hustadt, F. Papacchini, C. Nalon, C. Dixon. Model Construction for Modal Clauses.
  • H. Ihalainen, A. Oertel, Y. Kiam Tan, J. Berg, M. Järvisalo, M.O. Myreen, J. Nordström. Certified MaxSAT Preprocessing.
  • J.-C. Kassing, G. Vartanyan, J. Giesl. A Dependency Pair Framework for Relative Termination of Term Rewriting.
  • P. Lammich. Fast and Verified UNSAT Certificate Checking.
  • J. Mei, M. Bonsangue, A. Laarman. Equivalence Checking of Quantum Circuits by Model Counting.
  • J. Niederhauser, C.E. Brown, C. Kaliszyk. Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic.
  • D. Pattinson, C. Nalon. Non-Iterative Modal Resolution.
  • A. Pommellet, D. Stan, S. Scatton. SAT-based Learning of Computation Tree Logic.
  • E. Prebet, A. Platzer. Uniform Substitution for Differential Refinement Logic.
  • J. Rooduijn, D. Kozen, A. Silva. A cyclic proof system for Guarded Kleene Algebra with Tests.
  • H. Ruess. A Decision Method for First-Order Stream Logic.
  • J. Schöpf, F. Mitterwallner, A. Middeldorp. Confluence of Logically Constrained Rewrite Systems Revisited.
  • G. Sutcliffe, C. Suttner, L. Kotthoff, C. Raymond Perrault, Z. Khalid. An Empirical Assessment of Progress in Automated Theorem Proving.
  • N. Tsiskaridze, C. Barrett, C. Tinelli. An Abstract Calculus for Optimization Modulo Theories.
  • U. Waldmann. On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus.

Short papers

  • A. Bhayat, M. Suda. A Higher-Order Vampire.
  • S. Chassot, V. Kunčak. Verifying a Realistic Mutable Hash Table: Case Study.
  • A. De Lon. The Naproche-ZF theorem prover.
  • T. Hader, D. Kaufmann, A. Irfan, S. Graham-Lengrand, L. Kovács. MCSat-based Finite Field Reasoning in the Yices2 SMT Solver.
  • M. Heisinger, S. Heisinger, M. Seidl. Booleguru, the Propositional Polyglot.
  • N. Lommen, E. Meyer, J. Giesl. Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT.