default search action
11th IJCAR 2022: Haifa, Israel
- Jasmin Blanchette
, Laura Kovács
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
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
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
SAT-Based Proof Search in Intermediate Propositional Logics. 57-74 - Hannes Ihalainen
Clause Redundancy and Preprocessing in Maximum Satisfiability. 75-94 - Gereon Kremer
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). 95-105 - Joseph E. Reeves
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
Reasoning About Vectors Using an SMT Theory of Sequences. 125-143
Calculi and Orderings
- Martin Bromberger
An Efficient Subsumption Test Pipeline for BS(LRA) Clauses. 147-168 - André Duarte
Ground Joinability and Connectedness in the Superposition Calculus. 169-187 - Fajar Haifani
Connection-Minimal Abduction in EL via Translation to FOL. 188-207 - Fajar Haifani
Semantic Relevance. 208-227 - Hendrik Leidinger
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
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
GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description). 300-309 - Hui Yang
Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications. 310-328
Choices, Invariance, Substitutions, and Formalizations
- Michael Bernreiter, Anela Lolic, Jan Maly
Sequent Calculi for Choice Logics. 331-349 - Chad E. Brown, Cezary Kaliszyk
Lash 1.0 (System Description). 350-358 - Julie Cailler
Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). 359-368 - Stepan Holub, Martin Raska
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
Synthetic Tableaux: Minimal Tableau Search Heuristics. 407-425
Modal Logics
- Marta Bílková
Paraconsistent Gödel Modal Logic. 429-448 - Eben Blaisdell, Max I. Kanovich, Stepan L. Kuznetsov
Non-associative, Non-commutative Multi-modal Linear Logic. 449-467 - Ori Lahav
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices. 468-485 - Cláudia Nalon
Local Reductions for the Modal Cube. 486-505
Proof Systems and Proof Search
- Anupam Das
Cyclic Proofs, Hypersequents, and Transitive Closure Logic. 509-528 - Francisco Durán
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
Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. 559-577 - Temur Kutsia
A Framework for Approximate Generalization in Quantitative Theories. 578-596 - Jelle Piepenbrock
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
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
On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices. 671-690 - Marius Bozga
Decision Problems in a Logic for Reasoning About Reconfigurable Distributed Systems. 691-711 - Florian Frohn
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description). 712-722 - James Gallicchio
Implicit Definitions with Differential Equations for KeYmaera X - (System Description). 723-733 - Nils Lommen
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 2024-12-19 22:21 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: