Alessandro Armando, Peter Baumgartner, Gilles Dowek
Proceedings of the Fourth International Joint Conference on Automated Reasoning
IJCAR, 2008.

@proceedings{IJCAR-2008,
	address       = "Sydney, Australia",
	editor        = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
	isbn          = "978-3-540-71069-1",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fourth International Joint Conference on Automated Reasoning}",
	volume        = 5195,
	year          = 2008,
}

Contents (44 items)

14 ×#logic
9 ×#automation
9 ×#proving
8 ×#named
5 ×#theorem proving
3 ×#complexity
3 ×#reasoning
2 ×#analysis
2 ×#automaton
2 ×#challenge

IJCAR-2008-Gupta #automation #challenge #verification

Software Verification: Roles and Challenges for Automatic Decision Procedures (AG), p. 1.

IJCAR-2008-Melquiond #bound #proving

Proving Bounds on Real-Valued Functions with Computations (GM), pp. 2–17.

IJCAR-2008-Nipkow #linear #quantifier

Linear Quantifier Elimination (TN), pp. 18–33.

IJCAR-2008-BozgaIP #logic #source code

Quantitative Separation Logic and Programs with Lists (MB, RI, SP), pp. 34–49.

IJCAR-2008-HofnerS #automation #calculus #on the

On Automating the Calculus of Relations (PH, GS), pp. 50–66.

IJCAR-2008-GhilardiNRZ #model checking #smt #towards

Towards SMT Model Checking of Array-Based Systems (SG, EN, SR, DZ), pp. 67–82.

IJCAR-2008-BartheGP #java #proving #virtual machine

Preservation of Proof Obligations from Java to the Java Virtual Machine (GB, BG, MP), pp. 83–99.

IJCAR-2008-DarvasMR #performance

Efficient Well-Definedness Checking (ÁD, FM, AR), pp. 100–115.

IJCAR-2008-KremerMT #protocol #proving

Proving Group Protocols Secure Against Eavesdroppers (SK, AM, RT), pp. 116–131.

IJCAR-2008-AvanziniMS #analysis #automation #complexity

Automated Implicit Computational Complexity Analysis (MA, GM, AS), pp. 132–138.

IJCAR-2008-FurbachGHP #named

LogAnswer — A Deduction-Based Question Answering System (UF, IG, HH, BP), pp. 139–146.

IJCAR-2008-BeierleKK #automation #implementation #reasoning

A High-Level Implementation of a System for Automated Reasoning with Default Rules (CB, GKI, NK), pp. 147–153.

IJCAR-2008-Gacek #interactive #proving #theorem proving

The Abella Interactive Theorem Prover (AG), pp. 154–161.

IJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #proving #theorem proving

LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (CB, LCP, FT, AF), pp. 162–170.

IJCAR-2008-PlatzerQ #hybrid #named #proving #theorem proving

KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (AP, JDQ), pp. 171–178.

IJCAR-2008-Lutz #complexity #logic #query

The Complexity of Conjunctive Query Answering in Expressive Description Logics (CL), pp. 179–193.

IJCAR-2008-SchmidtT #first-order #logic

A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments (RAS, DT), pp. 194–209.

IJCAR-2008-KaminskiS #difference #hybrid #logic

Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse (MK, GS), pp. 210–225.

IJCAR-2008-BaaderP #axiom

Automata-Based Axiom Pinpointing (FB, RP), pp. 226–241.

IJCAR-2008-MotikH #logic #reasoning #reuse

Individual Reuse in Description Logic Reasoning (BM, IH), pp. 242–258.

IJCAR-2008-KonevWW #difference #logic #problem

The Logical Difference Problem for Description Logic Terminologies (BK, DW, FW), pp. 259–274.

IJCAR-2008-Kovacs #generative #invariant #named

Aligator: A Mathematica Package for Invariant Generation (LK), pp. 275–282.

IJCAR-2008-Otten #agile #logic #performance #proving #theorem proving

leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (JO), pp. 283–291.

IJCAR-2008-Korovin #first-order #logic #named #proving #theorem proving

iProver — An Instantiation-Based Theorem Prover for First-Order Logic (KK), pp. 292–298.

IJCAR-2008-GoreP #evaluation

An Experimental Evaluation of Global Caching for (RG, LP), pp. 299–305.

IJCAR-2008-SatoWKM #multi #termination #tool support

Multi-completion with Termination Tools (HS, SW, MK, AM), pp. 306–312.

IJCAR-2008-DuranLM #maude #named #termination

MTT: The Maude Termination Tool (FD, SL, JM), pp. 313–319.

IJCAR-2008-Schack-NielsenS #concurrent #deduction #framework #logic #named

Celf — A Logical Framework for Deductive and Concurrent Systems (ASN, CS), pp. 320–326.

IJCAR-2008-Dershowitz #exclamation

Canonicity! (ND), pp. 327–331.

IJCAR-2008-TourEN #equation #unification

Unification and Matching Modulo Leaf-Permutative Equational Presentations (TBdlT, ME, PN), pp. 332–347.

IJCAR-2008-Oostrom #composition #confluence

Modularity of Confluence (VvO), pp. 348–363.

IJCAR-2008-HirokawaM #analysis #automation #complexity #dependence

Automated Complexity Analysis Based on the Dependency Pair Method (NH, GM), pp. 364–379.

IJCAR-2008-BonacinaD #canonical

Canonical Inference for Implicational Systems (MPB, ND), pp. 380–395.

IJCAR-2008-Comon-Lundh #automation #challenge #protocol #security #verification

Challenges in the Automated Verification of Security Protocols (HCL), pp. 396–409.

IJCAR-2008-MouraB #effectiveness #logic #set #using

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets (LMdM, NB), pp. 410–425.

IJCAR-2008-PerezV #effectiveness #logic #proving

Proof Systems for Effectively Propositional Logic (JANP, AV), pp. 426–440.

IJCAR-2008-UrbanSPV #automation #reasoning #semantics

MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance (JU, GS, PP, JV), pp. 441–456.

IJCAR-2008-Sutcliffe #contest

CASC-J4 The 4th IJCAR ATP System Competition (GS), pp. 457–458.

IJCAR-2008-FietzkeW

Labelled Splitting (AF, CW), pp. 459–474.

IJCAR-2008-MouraB08a

Engineering DPLL(T) + Saturation (LMdM, NB), pp. 475–490.

IJCAR-2008-BenzmullerRS #higher-order #logic #named

THF0 — The Core of the TPTP Language for Higher-Order Logic (CB, FR, GS), pp. 491–506.

IJCAR-2008-NigamM #linear #logic

Focusing in Linear Meta-logic (VN, DM), pp. 507–522.

IJCAR-2008-BoyerGJ #automaton

Certifying a Tree Automata Completion Checker (BB, TG, TPJ), pp. 523–538.

IJCAR-2008-BouhoulaJ #automation #automaton #induction

Automated Induction with Constrained Tree Automata (AB, FJ), pp. 539–554.