Didier Galmiche, Stephan Schulz 0001, Roberto Sebastiani
Proceedings of the Ninth International Joint Conference on Automated Reasoning
IJCAR, 2018.

@proceedings{IJCAR-2018,
	doi           = "10.1007/978-3-319-94205-6",
	editor        = "Didier Galmiche and Stephan Schulz 0001 and Roberto Sebastiani",
	isbn          = "['978-3-319-94204-9', '978-3-319-94205-6']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Ninth International Joint Conference on Automated Reasoning}",
	volume        = 10900,
	year          = 2018,
}

Contents (46 items)

IJCAR-2018-LagniezBLM #approach #problem #satisfiability

An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem (JML, DLB, TdL, VM), pp. 1–18.

IJCAR-2018-ZhaoS #automation #logic #named #semantics

FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (YZ, RAS), pp. 19–27.

IJCAR-2018-BentkampBCW #higher-order #logic

Superposition for Lambda-Free Higher-Order Logic (AB, JCB, SC, UW), pp. 28–46.

IJCAR-2018-HannulaL #automation #reasoning #set

Automated Reasoning About Key Sets (MH, SL), pp. 47–63.

IJCAR-2018-LettmannP #calculus #proving

A Tableaux Calculus for Reducing Proof Size (MPL, NP), pp. 64–80.

IJCAR-2018-RappM

FORT 2.0 (FR, AM), pp. 81–88.

IJCAR-2018-SchlichtkrullBT #formal method #order #proving

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (AS, JCB, DT, UW), pp. 89–107.

IJCAR-2018-SteenB #higher-order #proving

The Higher-Order Prover Leo-III (AS, CB), pp. 108–116.

IJCAR-2018-DawsonDG

Well-Founded Unions (JED, ND, RG), pp. 117–133.

IJCAR-2018-FazekasBB #algorithm #modulo theories #satisfiability #set

Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (KF, FB, AB), pp. 134–151.

IJCAR-2018-ConchonDZ #memory management #model checking

Cubicle- W : Parameterized Model Checking on Weak Memory (SC, DD, FZ), pp. 152–160.

IJCAR-2018-LonsingE

QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (FL, UE), pp. 161–177.

IJCAR-2018-MelquiondR #algorithm #framework #proving #why

A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms (GM, RRH), pp. 178–193.

IJCAR-2018-FingerP #logic #probability #satisfiability

Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic (MF, SP), pp. 194–210.

IJCAR-2018-Platzer #difference #game studies #logic

Uniform Substitution for Differential Game Logic (AP), pp. 211–227.

IJCAR-2018-KanovichKNS #commutative #framework #logic

A Logical Framework with Commutative and Non-commutative Subexponentials (MIK, SK, VN, AS), pp. 228–245.

IJCAR-2018-ZeljicBWR #approximate #float #using

Exploring Approximations for Floating-Point Arithmetic Using UppSAT (AZ, PB, CMW, PR), pp. 246–262.

IJCAR-2018-BodirskyG #complexity #constraints #problem

Complexity of Combinations of Qualitative Constraint Satisfaction Problems (MB, JG), pp. 263–278.

IJCAR-2018-EchenimPS #framework #generative #modulo theories

A Generic Framework for Implicate Generation Modulo Theories (ME, NP, YS), pp. 279–294.

IJCAR-2018-CiobacaL #approach #induction #proving #reachability #term rewriting

A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems (SC, DL), pp. 295–311.

IJCAR-2018-GeMLZM #algorithm #approximate #probability

A New Probabilistic Algorithm for Approximate Model Counting (CG, FM, TL, JZ0, XM), pp. 312–328.

IJCAR-2018-Bromberger #bound #linear #problem #reduction

A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (MB), pp. 329–345.

IJCAR-2018-HirokawaNM #confluence #framework #tool support

Cops and CoCoWeb: Infrastructure for Confluence Tools (NH, JN, AM), pp. 346–353.

IJCAR-2018-HuangMGZZ #satisfiability #scalability #testing

Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PH0, FM, CG, JZ0, HZ), pp. 354–369.

IJCAR-2018-BlanchettePR #data type

Superposition with Datatypes and Codatatypes (JCB, NP, SR), pp. 370–387.

IJCAR-2018-ClaessenS #encoding #equation #first-order #logic #performance

Efficient Encodings of First-Order Horn Formulas in Equational Logic (KC, NS), pp. 388–404.

IJCAR-2018-KotelnikovKV #encoding #imperative #source code

A FOOLish Encoding of the Next State Relations of Imperative Programs (EK, LK, AV), pp. 405–421.

IJCAR-2018-Larchey-Wendling

Constructive Decision via Redundancy-Free Proof-Search (DLW), pp. 422–438.

IJCAR-2018-JeannerodT #algebra #first-order

Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (NJ, RT), pp. 439–454.

IJCAR-2018-KatelaanJW #automation #logic #modelling

A Separation Logic with Data: Small Models and Automation (JK, DJ, GW), pp. 455–471.

IJCAR-2018-WinklerM #named #order

MædMax: A Maximal Ordered Completion Tool (SW, GM), pp. 472–480.

IJCAR-2018-AcclavioS #combinator #proving

From Syntactic Proofs to Combinatorial Proofs (MA, LS), pp. 481–497.

IJCAR-2018-NalonP #calculus #logic

A Resolution-Based Calculus for Preferential Logics (CN, DP), pp. 498–515.

IJCAR-2018-KieslRH

Extended Resolution Simulates DRAT (BK, ARP, MJHH), pp. 516–531.

IJCAR-2018-ZhanH #complexity #imperative #source code #verification

Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (BZ, MPLH), pp. 532–548.

IJCAR-2018-HoenickeS #array #formal method #performance

Efficient Interpolation for the Theory of Arrays (JH, TS), pp. 549–565.

IJCAR-2018-PiotrowskiU #feedback #learning #named

ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (BP, JU), pp. 566–574.

IJCAR-2018-MullerRK

Theories as Types (DM0, FR, MK), pp. 575–590.

IJCAR-2018-ReynoldsVBTB #data type

Datatypes with Shared Selectors (AR, AV, HB, CT, CWB), pp. 591–608.

IJCAR-2018-KazakovS #using

Enumerating Justifications Using Resolution (YK, PS), pp. 609–626.

IJCAR-2018-IgnatievPNM #approach #satisfiability #set

A SAT-Based Approach to Learn Explainable Decision Sets (AI, FP, NN, JMS0), pp. 627–645.

IJCAR-2018-HoAKMTN #monad #synthesis

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (SH, OA, RK, MOM, YKT, MN), pp. 646–662.

IJCAR-2018-HernandezK #abstraction #framework #reasoning #scalability

An Abstraction-Refinement Framework for Reasoning with Large Theories (JCLH, KK), pp. 663–679.

IJCAR-2018-UrbaniKJDC #logic #performance

Efficient Model Construction for Horn Logic with VLog - System Description (JU, MK, CJHJ, ID, DC), pp. 680–688.

IJCAR-2018-Das #polynomial

Focussing, MALL and the Polynomial Hierarchy (AD0), pp. 689–705.

IJCAR-2018-PayetS #abstract interpretation #array #bound

Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (ÉP, FS), pp. 706–722.