default search action
10th IJCAR 2020: Paris, France
- Nicolas Peltier, Viorica Sofronie-Stokkermans:
Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. Lecture Notes in Computer Science 12166, Springer 2020, ISBN 978-3-030-51073-2
Invited Paper
- Ruzica Piskac
:
Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints. 3-10
SAT, SMT and QBF
- Marek S. Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, Zvonimir Rakamaric:
An SMT Theory of Fixed-Point Arithmetic. 13-31 - Lee A. Barnett
Covered Clauses Are Not Propagation Redundant. 32-47 - Joshua Brakensiek, Marijn Heule
The Resolution of Keller's Conjecture. 48-65 - Leroy Chew
How QBF Expansion Makes Strategy Extraction Hard. 66-82 - Emanuele De Angelis
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates. 83-102 - Stéphane Graham-Lengrand, Dejan Jovanovic, Bruno Dutertre:
Solving Bitvectors with MCSAT: Explanations from Bits and Pieces. 103-121 - Matthew Hague
Monadic Decomposition in Integer Linear Arithmetic. 122-140 - Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. 141-160
Decision Procedures and Combination of Theories
- Franz Baader
Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols. 163-180 - Diego Calvanese, Silvio Ghilardi, Alessandro Gianola
Combined Covers and Beth Definability. 181-200 - Timm Lampert
Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of Superpostulates. 201-217 - Andrew Reynolds
A Decision Procedure for String to Code Point Conversion. 218-237 - Ying Sheng
Politeness for the Theory of Algebraic Datatypes. 238-255
Superposition
- Ahmed Bhayat
A Knuth-Bendix-Like Ordering for Orienting Combinator Equations. 259-277 - Ahmed Bhayat
A Combinator-Based Superposition Calculus for Higher-Order Logic. 278-296 - Bernhard Gleiss, Laura Kovács
Subsumption Demodulation in First-Order Theorem Proving. 297-315 - Uwe Waldmann
A Comprehensive Framework for Saturation Theorem Proving. 316-334
Proof Procedures
- Peter Baumgartner:
Possible Models Computation and Revision - A Practical Approach. 337-355 - Maria Paola Bonacina, Sarah Winkler
SGGS Decision Procedures. 356-374 - Liron Cohen
Integrating Induction and Coinduction via Closure Operators and Proof Cycles. 375-394 - Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer:
Logic-Independent Proof Search in Logical Frameworks - (Short Paper). 395-401 - Bernhard Gleiss, Martin Suda:
Layered Clause Selection for Theory Reasoning - (Short Paper). 402-409
Non Classical Logics
- Franz Baader
Description Logics with Concrete Domains and General Concept Inclusions Revisited. 413-431 - David A. Basin, Thibault Dardinier
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic. 432-453 - Rose Bohrer
Constructive Hybrid Games. 454-473 - Asta Halkjær From
Formalizing a Seligman-Style Tableau System for Hybrid Logic - (Short Paper). 474-481 - Daniel Hausmann
NP Reasoning in the Monotone μ-Calculus. 482-499 - Max I. Kanovich, Stepan L. Kuznetsov
Soft Subexponentials and Multiplexing. 500-517 - Yiming Xu, Michael Norrish
Mechanised Modal Model Theory. 518-533
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-18 18:34 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: