Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings (Q5941850)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Jones, Neil D.}, Program termination analysis by size-change graphs (abstract), 1-4 [Zbl 0988.68732] \textit{Paulson, Lawrence C.}, SET cardholder registration: The secrecy proofs (extended abstract), 5-12 [Zbl 0988.68739] \textit{Voronkov, Andrei}, Algorithms, datastructures, and other issues in efficient automated deduction, 13-28 [Zbl 0988.68585] \textit{Haarslev, Volker; Möller, Ralf; Wessel, Michael}, The description logic \(\mathcal{ALCNH}_{R+}\) extended with concrete domains: A practically motivated approach, 29-44 [Zbl 0988.68182] \textit{Lutz, Carsten}, NEXPTIME-complete description logics with concrete domains, 45-60 [Zbl 0988.68175] \textit{Haarslev, Volker; Möller, Ralf; Turhan, Anni-Yasmin}, Exploiting pseudo models for TBox and ABox reasoning in expressive description logics, 61-75 [Zbl 0988.68181] \textit{Sattler, Ulrike; Vardi, Moshe Y.}, The hybrid \(\mu\)-calculus, 76-91 [Zbl 0988.03053] \textit{Baader, Franz; Tobies, Stephan}, The inverse method implements the automata approach for modal satisfiability, 92-106 [Zbl 0988.03021] \textit{Pliuškevičius, Regimantas}, Deduction-based decision procedure for a clausal miniscoped fragment of FTL, 107-120 [Zbl 0988.03018] \textit{Lutz, Carsten; Sturm, Holger; Wolter, Frank; Zakharyaschev, Michael}, Tableaux for temporal description logic with constant domains, 121-136 [Zbl 0988.68178] \textit{Cerrito, Serenella; Cialdea Mayer, Marta}, Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation, 137-151 [Zbl 0988.03032] \textit{Formisano, Andrea; Omodeo, Eugenio G.; Temperini, Marco}, Instructing equational set-reasoning with Otter, 152-167 [Zbl 0988.68164] \textit{Szeider, Stefan}, NP-completeness of refutability by literal-once resolution, 168-181 [Zbl 0988.03020] \textit{Hähnle, Reiner; Murray, Neil V.; Rosenthal, Erik}, Ordered resolution vs. connection graph resolution, 182-194 [Zbl 0990.68539] \textit{Stuber, Jürgen}, A model-based completeness proof of extended narrowing and resolution, 195-210 [Zbl 0988.03016] \textit{de Nivelle, Hans; Pratt-Hartmann, Ian}, A resolution-based decision procedure for the two-variable fragment with equality, 211-225 [Zbl 0988.03023] \textit{Waldmann, Uwe}, Superposition and chaining for totally ordered divisible abelian groups (extended abstract), 226-241 [Zbl 0988.03510] \textit{Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar}, Context trees, 242-256 [Zbl 0988.68588] \textit{Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei}, On the evaluation of indexing techniques for theorem proving, 257-271 [Zbl 0988.68595] \textit{Doutre, Sylvie; Mengin, Jérôme}, Preferred extensions of argumentation frameworks: Query, answering, and computation, 272-288 [Zbl 0990.68541] \textit{Armelín, Pablo A.; Pym, David J.}, Bunched logic programming (extended abstract), 289-304 [Zbl 0988.68508] \textit{Wang, Kewen}, A top-down procedure for disjunctive well-founded semantics, 305-317 [Zbl 0988.68032] \textit{Beeson, Michael}, A second-order theorem prover applied to circumscription, 318-324 [Zbl 0988.68583] \textit{Anger, Christian; Konczak, Kathrin; Linke, Thomas}, \texttt{NoMoRe}: A system for non-monotonic reasoning with logic programs under answer set semantics, 325-330 [Zbl 0988.68518] \textit{Benedetti, Marco}, Conditional pure literal graphs, 331-346 [Zbl 0990.68131] \textit{Giunchiglia, Enrico; Maratea, Massimo; Tacchella, Armando; Zambonin, Davide}, Evaluating search heuristics and optimization techniques in propositional satisfiability, 347-363 [Zbl 0988.68608] \textit{Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando}, QUBE: A system for deciding quantified Boolean formulas satisfiability, 364-369 [Zbl 0988.68598] \textit{Schulz, Stephan}, System abstract: E 0. 61, 370-375 [Zbl 0988.68602] \textit{Riazanov, Alexandre; Voronkov, Andrei}, Vampire 1. 1 (system description), 376-380 [Zbl 0988.68607] \textit{Letz, Reinhold; Stenz, Gernot}, DCTP -- a disconnection calculus theorem prover -- system abstract, 381-385 [Zbl 0988.68589] \textit{Luther, Marko}, More on implicit syntax, 386-400 [Zbl 0988.68593] \textit{Pientka, Brigitte}, Termination and reduction checking for higher-order logic programs, 401-415 [Zbl 0988.68514] \textit{Fiedler, Armin}, P. rex: An interactive proof explainer, 416-420 [Zbl 0988.68596] \textit{Schmitt, Stephan; Lorigo, Lori; Kreitz, Christoph; Nogin, Aleksey}, JProver: Integrating connection-based theorem proving into interactive proof assistants, 421-426 [Zbl 0988.68609] \textit{Audemard, Gilles; Henocque, Laurent}, The eXtended least number heuristic, 427-442 [Zbl 0988.68605] \textit{Hodgson, Kahlil; Slaney, John}, System description: SCOTT-5, 443-447 [Zbl 0988.68603] \textit{Bonacina, Maria Paola}, Combination of distributed search and multi-search in peers-mcd. d. (system description), 448-452 [Zbl 0988.68611] \textit{Fariñas del Cerro, Luis; Fauthoux, David; Gasquet, Olivier; Herzig, Andreas; Longin, Dominique}, Lotrec: The generic tableau prover for modal and description logics, 453-458 [Zbl 0988.68592] \textit{Happe, Jens}, The MODPROF theorem prover, 459-463 [Zbl 0988.68606] \textit{Patel-Schneider, Peter F.; Sebastiani, Roberto}, A new system and methodology for generating random modal formulae, 464-468 [Zbl 0988.68582] \textit{Giesl, Jürgen; Kapur, Deepak}, Decidable classes of inductive theorems, 469-484 [Zbl 0988.03017] \textit{Urbain, Xavier}, Automated incremental termination proofs for hierarchically defined term rewriting systems, 485-498 [Zbl 0988.68094] \textit{Lynch, Christopher; Morawska, Barbara}, Decidability and complexity of finitely closable linear equational theories, 499-513 [Zbl 0988.03013] \textit{Ganzinger, Harald; McAllester, David}, A new meta-complexity theorem for bottom-up logic programs, 514-528 [Zbl 0988.68031] \textit{Avron, Arnon; Lev, Iddo}, Canonical propositional Gentzen-type systems, 529-544 [Zbl 0988.03011] \textit{Giese, Martin}, Incremental closure of free variable tableaux, 545-560 [Zbl 0988.03019] \textit{Egly, Uwe; Schmitt, Stephan}, Deriving modular programs from short proofs, 561-577 [Zbl 0988.03086] \textit{Peltier, Nicolas}, A general method for using schematizations in automated deduction, 578-592 [Zbl 0988.03015] \textit{Middeldorp, Aart}, Approximating dependency graphs using tree automata techniques, 593-610 [Zbl 0988.68162] \textit{Boigelot, Bernard; Jodogne, Sébastien; Wolper, Pierre}, On the use of weak automata for deciding linear arithmetic with integer and real variables, 611-625 [Zbl 0988.03022] \textit{Beckert, Bernhard; Schlager, Steffen}, A sequent calculus for first-order dynamic logic with trace modalities, 626-641 [Zbl 0988.03051] \textit{Reif, Wolfgang; Schellhorn, G.; Thums, Andreas}, Flaw detection in formal specifications, 642-657 [Zbl 0988.68107] \textit{Avenhaus, Jürgen; Löchner, Bernd}, CCE: Testing ground joinability, 658-662 [Zbl 0988.68587] \textit{Armando, Alessandro; Compagna, Luca; Ranise, Silvio}, System description: RDL: Rewrite and Decision procedure Laboratory, 663-669 [Zbl 0988.68557] \textit{Hodas, Joshua S.; Tamura, Naoyuki}, lolliCoP -- a linear logic implementation of a lean connection-method theorem prover for first-order classical logic, 670-684 [Zbl 0988.68610] \textit{Pastre, Dominique}, MUSCADET 2. 3: A knowledge-based theorem prover based on natural deduction, 685-689 [Zbl 0988.68594] \textit{Lücke, Jörg}, Hilberticus -- a tool deciding an elementary sublanguage of set theory, 690-695 [Zbl 0988.68591] \textit{Larchey-Wendling, D.; Méry, D.; Galmiche, Didier}, STRIP: Structural sharing for efficient proof-search, 696-700 [Zbl 0990.68540] \textit{Haarslev, Volker; Möller, Ralf}, RACER system description, 701-705 [Zbl 0988.68599]