Rajeev Goré, Alexander Leitsch, Tobias Nipkow
Proceedings of the First International Joint Conference on Automated Reasoning
IJCAR, 2001.

@proceedings{IJCAR-2001,
	address       = "Siena, Italy",
	editor        = "Rajeev Goré and Alexander Leitsch and Tobias Nipkow",
	isbn          = "3-540-42254-4",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the First International Joint Conference on Automated Reasoning}",
	volume        = 2083,
	year          = 2001,
}

Contents (59 items)

13 ×#proving
8 ×#logic
7 ×#theorem proving
6 ×#named
4 ×#graph
4 ×#logic programming
4 ×#source code
3 ×#automation
3 ×#automaton
3 ×#calculus

IJCAR-2001-Jones #analysis #graph #termination

Program Termination Analysis by Size-Change Graphs (NDJ), pp. 1–4.

IJCAR-2001-Paulson #proving #set

SET Cardholder Registration: The Secrecy Proofs (LCP), pp. 5–12.

IJCAR-2001-Voronkov #algorithm #automation #deduction #performance

Algorithms, Datastructures, and other Issues in Efficient Automated Deduction (AV), pp. 13–28.

IJCAR-2001-HaarslevMW #approach #logic #motivation

The Description Logic ALCNHR+ Extended with Concrete Domains: A Practically Motivated Approach (VH, RM, MW), pp. 29–44.

IJCAR-2001-Lutz #logic

NEXPTIME-Complete Description Logics with Concrete Domains (CL), pp. 45–60.

IJCAR-2001-HaarslevMT #logic #modelling #pseudo #reasoning

Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics (VH, RM, AYT), pp. 61–75.

IJCAR-2001-SattlerV #calculus #hybrid

The Hybrid µ-Calculus (US, MYV), pp. 76–91.

IJCAR-2001-BaaderT #approach #automaton #satisfiability

The Inverse Method Implements the Automata Approach for Modal Satisfiability (FB, ST), pp. 92–106.

IJCAR-2001-Pliuskevicius

Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL (RP), pp. 107–120.

IJCAR-2001-LutzSWZ #constant #logic

Tableaux for Temporal Description Logic with Constant Domains (CL, HS, FW, MZ), pp. 121–136.

IJCAR-2001-CerritoM #logic #quantifier

Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation (SC, MCM), pp. 137–151.

IJCAR-2001-FormisanoOT #equation

Instructing Equational Set-Reasoning with Otter (AF, EGO, MT), pp. 152–167.

IJCAR-2001-Szeider

NP-Completeness of Refutability by Literal-Once Resolution (SS), pp. 168–181.

IJCAR-2001-HahnleMR #graph #order

Ordered Resolution vs. Connection Graph Resolution (RH, NVM, ER), pp. 182–194.

IJCAR-2001-Stuber #modelling #proving

A Model-Based Completeness Proof of Extended Narrowing and Resolution (JS), pp. 195–210.

IJCAR-2001-NivelleP #similarity

A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality (HdN, IPH), pp. 211–225.

IJCAR-2001-Waldmann #order

Superposition and Chaining for Totally Ordered Divisible Abelian Groups (UW), pp. 226–241.

IJCAR-2001-GanzingerNN

Context Trees (HG, RN, PN), pp. 242–256.

IJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving #theorem proving

On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.

IJCAR-2001-DoutreM #framework #query

Preferred Extensions of Argumentation Frameworks: Query Answering and Computation (SD, JM), pp. 272–288.

IJCAR-2001-ArmelinP #logic programming

Bunched Logic Programming (PAA, DJP), pp. 289–304.

IJCAR-2001-Wang #semantics #top-down

A Top-Down Procedure for Disjunctive Well-Founded Semantics (KW), pp. 305–317.

IJCAR-2001-Beeson #higher-order #proving #theorem proving

A Second-Order Theorem Prover Applied to Circumscription (MB), pp. 318–324.

IJCAR-2001-AngerKL #logic programming #reasoning #semantics #set #source code

NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics (CA, KK, TL), pp. 325–330.

IJCAR-2001-Benedetti #graph

Conditional Pure Literal Graphs (MB), pp. 331–346.

IJCAR-2001-GiunchigliaMTZ #heuristic #optimisation #satisfiability

Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability (EG, MM, AT, DZ), pp. 347–363.

IJCAR-2001-GiunchigliaNT #named #quantifier #satisfiability

QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability (EG, MN, AT), pp. 364–369.

IJCAR-2001-Schulz

System Abstract: E 0.61 (SS), pp. 370–375.

IJCAR-2001-RiazanovV

Vampire 1.1 (AR, AV), pp. 376–380.

IJCAR-2001-LetzS #calculus #named #proving #theorem proving

DCTP — A Disconnection Calculus Theorem Prover — System Abstract (RL, GS), pp. 381–385.

IJCAR-2001-Luther #syntax

More On Implicit Syntax (ML), pp. 386–400.

IJCAR-2001-Pientka #higher-order #logic programming #reduction #source code #termination

Termination and Reduction Checking for Higher-Order Logic Programs (BP), pp. 401–415.

IJCAR-2001-Fiedler #interactive #proving

P.rex: An Interactive Proof Explainer (AF), pp. 416–420.

IJCAR-2001-SchmittLKN #interactive #proving #theorem proving

JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.

IJCAR-2001-AudemardH #heuristic

The eXtended Least Number Heuristic (GA, LH), pp. 427–442.

IJCAR-2001-HodgsonS

System Description: SCOTT-5 (KH, JKS), pp. 443–447.

IJCAR-2001-Bonacina #distributed #multi

Combination of Distributed Search and Multi-search in Peers-mcd.d (MPB), pp. 448–452.

IJCAR-2001-CerroFGHLM #logic #proving

Lotrec : The Generic Tableau Prover for Modal and Description Logics (LFdC, DF, OG, AH, DL, FM), pp. 453–458.

IJCAR-2001-Happe #proving #theorem proving

The MODPROF Theorem Prover (JH), pp. 459–463.

IJCAR-2001-Patel-SchneiderS #generative #random

A New System and Methodology for Generating Random Modal Formulae (PFPS, RS), pp. 464–468.

IJCAR-2001-GieslK #decidability #induction #theorem

Decidable Classes of Inductive Theorems (JG, DK), pp. 469–484.

IJCAR-2001-Urbain #automation #incremental #proving #term rewriting #termination

Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems (XU), pp. 485–498.

IJCAR-2001-LynchM #complexity #decidability #equation #linear

Decidability and Complexity of Finitely Closable Linear Equational Theories (CL, BM), pp. 499–513.

IJCAR-2001-GanzingerM #bottom-up #logic programming #source code #theorem

A New Meta-complexity Theorem for Bottom-Up Logic Programs (HG, DAM), pp. 514–528.

IJCAR-2001-AvronL #canonical #type system

Canonical Propositional Gentzen-Type Systems (AA, IL), pp. 529–544.

IJCAR-2001-Giese #incremental

Incremental Closure of Free Variable Tableaux (MG), pp. 545–560.

IJCAR-2001-EglyS #composition #proving #source code

Deriving Modular Programs from Short Proofs (UE, SS), pp. 561–577.

IJCAR-2001-Peltier #automation #deduction #using

A General Method for Using Schematizations in Automated Deduction (NP), pp. 578–592.

IJCAR-2001-Middeldorp #approximate #automaton #dependence #graph #using

Approximating Dependency Graphs Using Tree Automata Techniques (AM), pp. 593–610.

IJCAR-2001-BoigelotJW #automaton #integer #linear #on the #using

On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables (BB, SJ, PW), pp. 611–625.

IJCAR-2001-BeckertS #calculus #first-order #logic

A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities (BB, SS), pp. 626–641.

IJCAR-2001-ReifST #detection #specification

Flaw Detection in Formal Specifications (WR, GS, AT), pp. 642–657.

IJCAR-2001-AvenhausL #named #testing

CCE: Testing Ground Joinability (JA, BL), pp. 658–662.

IJCAR-2001-ArmandoCR

System Description: RDL : Rewrite and Decision Procedure Laboratory (AA, LC, SR), pp. 663–669.

IJCAR-2001-HodasT #agile #first-order #implementation #linear #logic #named #proving #theorem proving

lolliCop — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic (JSH, NT), pp. 670–684.

IJCAR-2001-Pastre #deduction #knowledge-based #proving #theorem proving

MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction (DP), pp. 685–689.

IJCAR-2001-Lucke #named #set

Hilberticus — A Tool Deciding an Elementary Sublanguage of Set Theory (JL), pp. 690–695.

IJCAR-2001-Larchey-WendlingMG #named #performance

STRIP: Structural Sharing for Efficient Proof-Search (DLW, DM, DG), pp. 696–700.

IJCAR-2001-HaarslevM

RACER System Description (VH, RM), pp. 701–706.