Proceedings of the Ninth International Joint Conference on Automated Reasoning
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

TEST
DBLP
Scholar
DOI
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.