default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID11th IJCAR 2022: Haifa, Israel
- Jasmin Blanchette
, Laura Kovács, Dirk Pattinson:
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science 13385, Springer 2022, ISBN 978-3-031-10768-9
Invited Talks
- Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez, Albert Rubio:
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. 3-7 - Gilles Dowek:
From the Universality of Mathematical Truth to the Interoperability of Proof Systems. 8-11
Satisfiability, SMT Solving, and Arithmetic
- Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett:
Flexible Proof Production in an Industrial-Strength SMT Solver. 15-35 - Paolo Felli, Marco Montali, Sarah Winkler:
CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic. 36-56 - Camillo Fiorentini, Mauro Ferrari:
SAT-Based Proof Search in Intermediate Propositional Logics. 57-74 - Hannes Ihalainen, Jeremias Berg, Matti Järvisalo:
Clause Redundancy and Preprocessing in Maximum Satisfiability. 75-94 - Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). 95-105 - Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. 106-124 - Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli:
Reasoning About Vectors Using an SMT Theory of Sequences. 125-143
Calculi and Orderings
- Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach:
An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. 147-168 - André Duarte, Konstantin Korovin:
Ground Joinability and Connectedness in the Superposition Calculus. 169-187 - Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach:
Connection-Minimal Abduction in EL via Translation to FOL. 188-207 - Fajar Haifani, Christoph Weidenbach:
Semantic Relevance. 208-227 - Hendrik Leidinger, Christoph Weidenbach:
SCL(EQ): SCL for First-Order Logic with Equality. 228-247 - Akihisa Yamada:
Term Orderings for Non-reachability of (Conditional) Rewriting. 248-267
Knowledge Representation and Justification
- Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Raimund Dachselt, Patrick Koopmann, Julián Méndez:
Evonne: Interactive Proof Visualization for Description Logics (System Description). 271-280 - Claudia Cauli, Magdalena Ortiz, Nir Piterman:
Actions over Core-Closed Knowledge Bases. 281-299 - Tanel Tammet, Dirk Draheim, Priit Järv:
GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description). 300-309 - Hui Yang, Yue Ma, Nicole Bidoit:
Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications. 310-328
Choices, Invariance, Substitutions, and Formalizations
- Michael Bernreiter, Anela Lolic, Jan Maly, Stefan Woltran:
Sequent Calculi for Choice Logics. 331-349 - Chad E. Brown, Cezary Kaliszyk:
Lash 1.0 (System Description). 350-358 - Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde-Lilia Bouziane:
Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). 359-368 - Stepan Holub, Martin Raska, Stepán Starosta:
Binary Codes that Do Not Preserve Primitivity. 369-387 - Takuya Matsuzaki, Tomohiro Fujita:
Formula Simplification via Invariance Detection by Algebraically Indexed Types. 388-406 - Michal Sochanski, Dorota Leszczynska-Jasion, Szymon Chlebowski, Agata Tomczyk, Marcin Jukiewicz:
Synthetic Tableaux: Minimal Tableau Search Heuristics. 407-425
Modal Logics
- Marta Bílková, Sabine Frittella, Daniil Kozhemiachenko:
Paraconsistent Gödel Modal Logic. 429-448 - Eben Blaisdell, Max I. Kanovich, Stepan L. Kuznetsov, Elaine Pimentel, Andre Scedrov:
Non-associative, Non-commutative Multi-modal Linear Logic. 449-467 - Ori Lahav, Yoni Zohar:
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. 468-485 - Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon:
Local Reductions for the Modal Cube. 486-505
Proof Systems and Proof Search
- Anupam Das, Marianna Girlando:
Cyclic Proofs, Hypersequents, and Transitive Closure Logic. 509-528 - Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, Carolyn L. Talcott:
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description). 529-540 - Andrzej Indrzejczak:
Leśniewski's Ontology - Proof-Theoretic Characterization. 541-558 - Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson:
Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. 559-577 - Temur Kutsia, Cleo Pau:
A Framework for Approximate Generalization in Quantitative Theories. 578-596 - Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban:
Guiding an Automated Theorem Prover with Neural Rewriting. 597-617 - Andrei Popescu:
Rensets and Renaming-Based Recursion for Syntax with Bindings. 618-639 - Vitor Greati, João Marcos:
Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics. 640-658 - Martin Suda:
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description). 659-667
Evolution, Termination, and Decision Problems
- S. Akshay, Supratik Chakraborty, Debtanu Pal:
On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices. 671-690 - Marius Bozga, Lucas Bueri, Radu Iosif:
Decision Problems in a Logic for Reasoning About Reconfigurable Distributed Systems. 691-711 - Florian Frohn, Jürgen Giesl:
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description). 712-722 - James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer:
Implicit Definitions with Differential Equations for KeYmaera X - (System Description). 723-733 - Nils Lommen, Fabian Meyer, Jürgen Giesl:
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops. 734-754
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-02-21 19:42 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:
