default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID29th CADE 2023: Rome, Italy
- Brigitte Pientka
, Cesare Tinelli:
Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings. Lecture Notes in Computer Science 14132, Springer 2023, ISBN 978-3-031-38498-1 - Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Dieter Vandesande:
Certified Core-Guided MaxSAT Solving. 1-22 - Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson:
Superposition with Delayed Unification. 23-40 - Nikolaj S. Bjørner, Katalin Fazekas:
On Incremental Pre-processing for SMT. 41-60 - Jasmin Blanchette, Qi Qiu, Sophie Tourret:
Verified Given Clause Procedures. 61-77 - Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier:
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. 78-95 - Marvin Brieger, Stefan Mitsch, André Platzer:
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. 96-115 - Martin Bromberger, Martin Desharnais, Christoph Weidenbach:
An Isabelle/HOL Formalization of the SCL(FOL) Calculus. 116-133 - Martin Bromberger, Chaahat Jain, Christoph Weidenbach:
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning. 134-152 - Florian Bruse, Martin Lange, Sören Möller:
Formal Reasoning About Influence in Natural Sciences Experiments. 153-169 - Yu-Fang Chen, Philipp Rümmer, Wei-Lun Tsai:
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification). 170-189 - Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath:
SAT-Based Subsumption Resolution. 190-206 - Mathias Fleury, Peter Lammich:
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). 207-219 - Florian Frohn, Jürgen Giesl:
Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper). 220-233 - Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder:
COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description). 234-247 - Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler:
Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT. 248-265 - Jera Hensel, Jürgen Giesl:
Proving Termination of C Programs with Lists. 266-285 - Tomás Fiedor, Lukás Holík, Martin Hruska, Adam Rogalewicz, Juraj Síc, Pavol Vargovcík:
Reasoning About Regular Properties: A Comparative Study. 286-306 - Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov:
Program Synthesis in Saturation. 307-324 - Andrzej Indrzejczak, Yaroslav I. Petrukhin:
A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus. 325-343 - Jan-Christoph Kassing, Jürgen Giesl:
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs. 344-364 - Katharina Kreuzer, Tobias Nipkow:
Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. 365-381 - Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon:
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic. 382-400 - Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp:
Left-Linear Completion with AC Axioms. 401-418 - Dennis Peuter, Viorica Sofronie-Stokkermans, Sebastian Thunert:
On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics Eℒ, Eℒ+. 419-437 - Colin Rothgang, Florian Rabe, Christoph Benzmüller:
Theorem Proving in Dependently-Typed Higher-Order Logic. 438-455 - Manfred Schmidt-Schauß, Daniele Nantes-Sobrinho:
Towards Fast Nominal Anti-unification of Letrec-Expressions. 456-473 - Jonas Schöpf, Aart Middeldorp:
Confluence Criteria for Logically Constrained Rewrite Systems. 474-490 - Lukas Stevens:
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory. 491-508 - Tanel Tammet, Priit Järv, Martin Verrev, Dirk Draheim:
An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper). 509-521 - Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett:
Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness. 522-541 - Bernard Boigelot, Pascal Fontaine, Baptiste Vergain:
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. 542-559 - Gerald Whitters, Vivek Nigam, Carolyn L. Talcott:
Incremental Rewriting Modulo SMT. 560-576 - Bohua Zhan, Yuheng Fan, Weiqiang Xiong, Runqing Xu:
Iscalc: An Interactive Symbolic Computation Framework (System Description). 577-589
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-04 01:25 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
