Proceedings of the Seventh 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

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

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

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.

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.