default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID9th 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, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann:
Superposition for Lambda-Free Higher-Order Logic. 28-46 - Miika Hannula, Sebastian Link:
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, Dmitriy Traytel, Uwe Waldmann:
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, Fahiem Bacchus, Armin Biere:
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories. 134-151 - Sylvain Conchon, David Declerck, Fatiha Zaïdi:
Cubicle- W : Parameterized Model Checking on Weak Memory. 152-160 - Florian Lonsing, Uwe Egly:
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. 161-177 - Guillaume Melquiond, Raphaël Rieu-Helft:
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, Vivek Nigam, Andre Scedrov:
A Logical Framework with Commutative and Non-commutative Subexponentials. 228-245 - Aleksandar Zeljic, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer:
Exploring Approximations for Floating-Point Arithmetic Using UppSAT. 246-262 - Manuel Bodirsky, Johannes Greiner:
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, Julian Nagele, Aart Middeldorp:
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, Nicolas Peltier, Simon Robillard:
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, Andrei Voronkov:
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, Dejan Jovanovic, Georg Weissenbacher:
A Separation Logic with Data: Small Models and Automation. 455-471 - Sarah Winkler, Georg Moser:
MædMax: A Maximal Ordered Completion Tool. 472-480 - Matteo Acclavio, Lutz Straßburger:
From Syntactic Proofs to Combinatorial Proofs. 481-497 - Cláudia Nalon, Dirk Pattinson:
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, Tanja Schindler:
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, Florian Rabe, Michael Kohlhase:
Theories as Types. 575-590 - Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett:
Datatypes with Shared Selectors. 591-608 - Yevgeny Kazakov, Peter Skocovský:
Enumerating Justifications Using Resolution. 609-626 - Alexey Ignatiev, Filipe Pereira, Nina Narodytska, João Marques-Silva:
A SAT-Based Approach to Learn Explainable Decision Sets. 627-645 - Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish:
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, Markus Krötzsch, Ceriel J. H. Jacobs, Irina Dragoste, David Carral:
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 2025-12-09 23:36 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:
