Stéphane Demri, Deepak Kapur, Christoph Weidenbach
Proceedings of the Seventh International Joint Conference on Automated Reasoning
IJCAR, 2014.

@proceedings{IJCAR-2014,
	address       = "Vienna, Austria",
	doi           = "10.1007/978-3-319-08587-6",
	editor        = "Stéphane Demri and Deepak Kapur and Christoph Weidenbach",
	isbn          = "978-3-319-08586-9",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Seventh International Joint Conference on Automated Reasoning}",
	volume        = 8562,
	year          = 2014,
}

Contents (40 items)

19 ×#logic
10 ×#proving
7 ×#named
5 ×#satisfiability
4 ×#calculus
3 ×#theorem proving
2 ×#approximate
2 ×#automation
2 ×#axiom
2 ×#finite

IJCAR-2014-AvniKT #game studies #reachability #specification

From Reachability to Temporal Specifications in Cost-Sharing Games (GA, OK, TT), pp. 1–15.

IJCAR-2014-Cortier #how #logic

Electronic Voting: How Logic Can Help (VC), pp. 16–25.

IJCAR-2014-Gore #fixpoint #logic #ltl

And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (RG), pp. 26–45.

IJCAR-2014-Blanchette0T #induction #logic

Unified Classical Logic Completeness — A Coinductive Pearl (JCB, AP, DT), pp. 46–60.

IJCAR-2014-Lindblad #calculus #higher-order #logic

A Focused Sequent Calculus for Higher-Order Logic (FL), pp. 61–75.

IJCAR-2014-LahavZ #calculus #satisfiability

SAT-Based Decision Procedure for Analytic Pure Sequent Calculi (OL, YZ), pp. 76–90.

IJCAR-2014-HeuleSB #preprocessor #proving

A Unified Proof System for QBF Preprocessing (MH, MS, AB), pp. 91–106.

IJCAR-2014-AnsoteguiBGL #satisfiability

The Fractal Dimension of SAT Formulas (CA, MLB, JGC, JL), pp. 107–121.

IJCAR-2014-ChocronFR #satisfiability

A Gentle Non-disjoint Combination of Satisfiability Procedures (PC, PF, CR), pp. 122–136.

IJCAR-2014-EchenimPT #equation #logic

A Rewriting Strategy to Generate Prime Implicates in Equational Logic (ME, NP, ST), pp. 137–151.

IJCAR-2014-BaumgartnerBW #finite #proving #quantifier #theorem proving

Finite Quantification in Hierarchic Theorem Proving (PB, JB, UW), pp. 152–167.

IJCAR-2014-BerdineB #refinement #smt

Computing All Implied Equalities via SMT-Based Partition Refinement (JB, NB), pp. 168–183.

IJCAR-2014-GieslBEFFOPSSST #automation #proving #source code #termination

Proving Termination of Programs Automatically with AProVE (JG, MB, FE, FF, CF, CO, MP, PSK, TS, SS, RT), pp. 184–191.

IJCAR-2014-HorbachS #axiom #locality #reachability

Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (MH, VSS), pp. 192–207.

IJCAR-2014-StroderGBFFHS #memory management #pointer #proving #safety #source code #termination

Proving Termination and Memory Safety for Programs with Pointer Arithmetic (TS, JG, MB, FF, CF, JH, PSK), pp. 208–223.

IJCAR-2014-Zhang #encoding #verification

QBF Encoding of Temporal Properties and QBF-Based Verification (WZ), pp. 224–239.

IJCAR-2014-HetzlLRTW #logic #quantifier #similarity

Introducing Quantified Cuts in Logic with Equality (SH, AL, GR, JT, DW), pp. 240–254.

IJCAR-2014-NigamRL #automation #named #permutation #proving

Quati: An Automated Tool for Proving Permutation Lemmas (VN, GR, LL), pp. 255–261.

IJCAR-2014-GoreTW #logic #proving #theorem proving #using

A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description (RG, JT, JW), pp. 262–268.

IJCAR-2014-Otten #first-order #logic #named #proving

MleanCoP: A Connection Prover for First-Order Modal Logic (JO), pp. 269–276.

IJCAR-2014-CerritoDG #atl #logic #satisfiability #testing

Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+ (SC, AD, VG), pp. 277–291.

IJCAR-2014-JeanninP #difference #hybrid #logic #named

dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems (JBJ, AP), pp. 292–306.

IJCAR-2014-Lellmann #axiom #strict #theory and practice

Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (BL), pp. 307–321.

IJCAR-2014-NalonMD #confluence #logic

Clausal Resolution for Modal Logics of Confluence (CN, JM, CD), pp. 322–336.

IJCAR-2014-GoreOT #calculus #implementation #using

Implementing Tableau Calculi Using BDDs: BDDTab System Description (RG, KO, JT), pp. 337–343.

IJCAR-2014-ZeljicWR #approximate

Approximations for Model Construction (AZ, CMW, PR), pp. 344–359.

IJCAR-2014-EhlersL #approximate #finite #incremental #logic #satisfiability

A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (RE, ML), pp. 360–366.

IJCAR-2014-StumpST #framework #logic #named

StarExec: A Cross-Community Infrastructure for Logic Solving (AS, GS, CT), pp. 367–373.

IJCAR-2014-BoudouFP #named #proving

Skeptik: A Proof Compression System (JB, AF, BWP), pp. 374–380.

IJCAR-2014-PapacchiniS #generative #logic

Terminating Minimal Model Generation Procedures for Propositional Modal Logics (FP, RAS), pp. 381–395.

IJCAR-2014-GorinPSWW #algebra #hybrid #logic #named

Cool — A Generic Reasoner for Coalgebraic Hybrid Logics (DG, DP, LS, FW, TW), pp. 396–402.

IJCAR-2014-BeyersdorffC #complexity #proving #theorem proving

The Complexity of Theorem Proving in Circumscription and Minimal Entailment (OB, LC), pp. 403–417.

IJCAR-2014-BozzelliS #linear #logic

Visibly Linear Temporal Logic (LB, CS), pp. 418–433.

IJCAR-2014-KoopmannS

Count and Forget: Uniform Interpolation of 𝒮ℋ𝒬-Ontologies (PK, RAS), pp. 434–448.

IJCAR-2014-SteigmillerGL #algorithm #logic

Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures (AS, BG, TL), pp. 449–463.

IJCAR-2014-MartinezFGHH #ontology

EL-ifying Ontologies (DC, CF, BCG, PH, IH), pp. 464–479.

IJCAR-2014-CeylanP #logic

The Bayesian Description Logic ℬℰℒ (IIC, RP), pp. 480–494.

IJCAR-2014-BeesonW #geometry #proving

OTTER Proofs in Tarskian Geometry (MB, LW), pp. 495–510.

IJCAR-2014-OlivettiP #calculus #implementation #logic #named

NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics (NO, GLP), pp. 511–518.

IJCAR-2014-PeaseS #information management #ontology #scalability

Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (AP, SS), pp. 519–525.