default search action
9th IJCAR 2018: Oxford, UK
- Didier Galmiche, Stephan Schulz, Roberto Sebastiani:
Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. Lecture Notes in Computer Science 10900, Springer 2018, ISBN 978-3-319-94204-9 - Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail
:
An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem. 1-18 - Yizheng Zhao, Renate A. Schmidt:
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics. 19-27 - Alexander Bentkamp
Superposition for Lambda-Free Higher-Order Logic. 28-46 - Miika Hannula
Automated Reasoning About Key Sets. 47-63 - Michael Peter Lettmann, Nicolas Peltier:
A Tableaux Calculus for Reducing Proof Size. 64-80 - Franziska Rapp, Aart Middeldorp
FORT 2.0. 81-88 - Anders Schlichtkrull, Jasmin Christian Blanchette
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. 89-107 - Alexander Steen, Christoph Benzmüller
The Higher-Order Prover Leo-III. 108-116 - Jeremy E. Dawson, Nachum Dershowitz, Rajeev Goré:
Well-Founded Unions. 117-133 - Katalin Fazekas
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. 134-151 - Sylvain Conchon, David Declerck
Cubicle- W : Parameterized Model Checking on Weak Memory. 152-160 - Florian Lonsing
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. 161-177 - Guillaume Melquiond
A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. 178-193 - Marcelo Finger, Sandro Preto
Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic. 194-210 - André Platzer
Uniform Substitution for Differential Game Logic. 211-227 - Max I. Kanovich, Stepan L. Kuznetsov
A Logical Framework with Commutative and Non-commutative Subexponentials. 228-245 - Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger
Exploring Approximations for Floating-Point Arithmetic Using UppSAT. 246-262 - Manuel Bodirsky
Complexity of Combinations of Qualitative Constraint Satisfaction Problems. 263-278 - Mnacho Echenim, Nicolas Peltier, Yanis Sellami
A Generic Framework for Implicate Generation Modulo Theories. 279-294 - Stefan Ciobaca, Dorel Lucanu:
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. 295-311 - Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang, Xutong Ma:
A New Probabilistic Algorithm for Approximate Model Counting. 312-328 - Martin Bromberger:
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. 329-345 - Nao Hirokawa
Cops and CoCoWeb: Infrastructure for Confluence Tools. 346-353 - Pei Huang, Feifei Ma, Cunjing Ge, Jian Zhang, Hantao Zhang:
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing. 354-369 - Jasmin Christian Blanchette
Superposition with Datatypes and Codatatypes. 370-387 - Koen Claessen, Nicholas Smallbone:
Efficient Encodings of First-Order Horn Formulas in Equational Logic. 388-404 - Evgenii Kotelnikov, Laura Kovács
A FOOLish Encoding of the Next State Relations of Imperative Programs. 405-421 - Dominique Larchey-Wendling
Constructive Decision via Redundancy-Free Proof-Search. 422-438 - Nicolas Jeannerod, Ralf Treinen:
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates. 439-454 - Jens Katelaan
A Separation Logic with Data: Small Models and Automation. 455-471 - Sarah Winkler
MædMax: A Maximal Ordered Completion Tool. 472-480 - Matteo Acclavio
From Syntactic Proofs to Combinatorial Proofs. 481-497 - Cláudia Nalon
A Resolution-Based Calculus for Preferential Logics. 498-515 - Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule
Extended Resolution Simulates DRAT. 516-531 - Bohua Zhan, Maximilian P. L. Haslbeck
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. 532-548 - Jochen Hoenicke
Efficient Interpolation for the Theory of Arrays. 549-565 - Bartosz Piotrowski, Josef Urban:
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. 566-574 - Dennis Müller
Theories as Types. 575-590 - Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa
Datatypes with Shared Selectors. 591-608 - Yevgeny Kazakov, Peter Skocovský:
Enumerating Justifications Using Resolution. 609-626 - Alexey Ignatiev
A SAT-Based Approach to Learn Explainable Decision Sets. 627-645 - Son Ho, Oskar Abrahamsson
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. 646-662 - Julio César López-Hernández, Konstantin Korovin:
An Abstraction-Refinement Framework for Reasoning with Large Theories. 663-679 - Jacopo Urbani
Efficient Model Construction for Horn Logic with VLog - System Description. 680-688 - Anupam Das
Focussing, MALL and the Polynomial Hierarchy. 689-705 - Étienne Payet, Fausto Spoto
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions. 706-722
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-11-21 20:17 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: