12. LPAR 2005: Montego Bay, Jamaica

• Allen Van Gelder:
  Independently Checkable Proofs from Decision Procedures: Issues and Progress. 1
  
• Thomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi:
  Zap: Automated Theorem Proving for Software Analysis. 2-22
  
• Robert Nieuwenhuis, Albert Oliveras:
  Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. 23-46
  
• Douglas B. Lenat:
  Scaling Up: Computers vs. Common Sense. 47-47
  
• Alessandro Dal Palù, Agostino Dovier, Enrico Pontelli:
  A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem. 48-63
  
• Matthias M. Hölzl, John N. Crossley:
  Disjunctive Constraint Lambda Calculi. 64-78
  
• Yao Wu, Enrico Pontelli, Desh Ranjan:
  Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees. 79-94
  
• Christian Anger, Martin Gebser, Thomas Linke, André Neumann, Torsten Schaub:
  The nomore++ Approach to Answer Set Solving. 95-109
  
• Gopalan Nadathur, Xiaochu Qi:
  Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. 110-124
  
• Nachum Dershowitz:
  The Four Sons of Penrose. 125-138
  
• Angelo Montanari, Alberto Policriti, Nicola Vitacolonna:
  An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures. 139-153
  
• Bernhard Beckert, Kerry Trentelman:
  Second-Order Principles in Specification Languages for Object-Oriented Programs. 154-168
  
• Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec:
  Strong Normalization of the Dual Classical Sequent Calculus. 169-183
  
• Salvador Lucas, José Meseguer:
  Termination of Fair Computations in Term Rewriting. 184-198
  
• Jeroen Ketema, Jakob Grue Simonsen:
  On Confluence of Infinitary Combinatory Reduction Systems. 199-214
  
• Temur Kutsia, Mircea Marin:
  Matching with Regular Constraints. 215-229
  
• Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio:
  Recursive Path Orderings Can Also Be Incremental. 230-245
  
• Marc Bezem, Thierry Coquand:
  Automating Coherent Logic. 246-260
  
• Florina Piroi, Temur Kutsia:
  The Theorema Environment for Interactive Proof Development. 261-275
  
• Magnus Björk:
  A First Order Extension of Stålmarck's Method. 276-291
  
• Vladimir Aleksic, Anatoli Degtyarev:
  Regular Derivations in Basic Superposition-Based Calculi. 292-306
  
• Wieslaw Szwast, Lidia Tendera:
  On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity. 307-321
  
• Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta:
  Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. 322-336
  
• Hitoshi Ohsaki, Jean-Marc Talbot, Sophie Tison, Yves Roos:
  Monotone AC-Tree Automata. 337-351
  
• Elaine Pimentel, Dale Miller:
  On the Specification of Sequent Systems. 352-366
  
• Amine Chaieb, Tobias Nipkow:
  Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. 367-380
  
• Matthias Daum, Stefan Maus, Norbert Schirmer, Mohamed Nassim Seghir:
  Integration of a Software Model Checker into Isabelle. 381-395
  
• Deian Tabakov, Moshe Y. Vardi:
  Experimental Evaluation of Classical Automata Constructions. 396-411
  
• Wolfgang Ahrendt, Andreas Roth, Ralf Sasse:
  Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics. 412-426
  
• Christoph Walther, Stephan Schweitzer:
  Reasoning About Incompletely Defined Programs. 427-442
  
• Calvin Kai Fan Tang, Eugenia Ternovska:
  Model Checking Abstract State Machines with Answer Set Programming. 443-458
  
• Didier Galmiche, Daniel Méry:
  Characterizing Provability in . 459-473
  
• Harvey Tuch, Gerwin Klein:
  A Unified Memory Model for Pointers. 474-488
  
• Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi:
  Treewidth in Verification: Local vs. Global. 489-503
  
• Laura Bozzelli, Aniello Murano, Adriano Peron:
  Pushdown Module Checking. 504-518
  
• Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang:
  Functional Correctness Proofs of Encryption Algorithms. 519-533
  
• Annabelle McIver, Tjark Weber:
  Towards Automated Proof Support for Probabilistic Distributed Systems. 534-548
  
• David A. Basin, Sebastian Mödersheim, Luca Viganò:
  Algebraic Intruder Deductions. 549-564
  
• Maarten Mariën, Rudradeb Mitra, Marc Denecker, Maurice Bruynooghe:
  Satisfiability Checking for PC(ID). 565-579
  
• Allen Van Gelder:
  Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning. 580-594
  
• Haiou Shen, Hantao Zhang:
  Another Complete Local Search Method for SAT. 595-605
  
• Sylvie Coste-Marquis, Caroline Devred, Pierre Marquis:
  Inference from Controversial Arguments. 606-620
  
• Mehdi Dastani, Guido Governatori, Antonino Rotolo, Leendert W. N. van der Torre:
  Programming Cognitive Agents in Defeasible Logic. 621-636
  
• Jürgen Dix, Wolfgang Faber, V. S. Subrahmanian:
  The Relationship Between Reasoning About Privacy and Default Logics. 637-650
  
• Mikhail Sheremet, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev:
  Comparative Similarity, Tree Automata, and Diophantine Equations. 651-665
  
• Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato:
  Analytic Tableaux for KLM Preferential and Cumulative Logics. 666-681
  
• Dominique Larchey-Wendling:
  Bounding Resource Consumption with Gödel-Dummett Logics. 682-696
  
• Matthias Baaz, Rosalie Iemhoff:
  On Interpolation in Existence Logics. 697-711
  
• Henning Christiansen, Davide Martinenghi:
  Incremental Integrity Checking: Limitations and Possibilities. 712-727
  
• Carsten Fritz:
  Concepts of Automata Construction from LTL. 728-742
  

Last update Sun May 19 23:08:09 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page