Abstract is missing.
- Monodic fragments of first-order temporal logics: 2000-2001 A.DIan M. Hodkinson, Frank Wolter, Michael Zakharyaschev. 1-23 [doi]
- On Bounded SpecificationsOrna Kupferman, Moshe Y. Vardi. 24-38 [doi]
- Improving Automata Generation for Linear Temporal Logic by Considering the Automaton HierarchyKlaus Schneider. 39-54 [doi]
- Local Temporal Logic is Expressively Complete for Cograph Dependence AlphabetsVolker Diekert, Paul Gastin. 55-69 [doi]
- Games and Model Checking for Guarded LogicsDietmar Berwanger, Erich Grädel. 70-84 [doi]
- Computational Space Efficiency and Minimal Model Generation for Guarded FormulaeLilia Georgieva, Ullrich Hustadt, Renate A. Schmidt. 85-99 [doi]
- Logical Omniscience and the Cost of DeliberationNatasha Alechina, Brian Logan. 100-109 [doi]
- Local Conditional High-Level Robot ProgramsSebastian Sardiña. 110-124 [doi]
- A Refinement Theory that Supports Reasoning About Knowledge and TimeKai Engelhardt, Ron van der Meyden, Yoram Moses. 125-141 [doi]
- Automated Theorem Proving Proof and Model Generation with Disconnection TableauxReinhold Letz, Gernot Stenz. 142-156 [doi]
- Counting the Number of Equivalent Binary Resolution ProofsJoseph D. Horton. 157-171 [doi]
- Splitting Through New Proposition SymbolsHans de Nivelle. 172-185 [doi]
- Complexity of Linear Standard TheoriesChristopher Lynch, Barbara Morawska. 186-200 [doi]
- Herbrand s Theorem for Prenex Gödel Logic and its Consequences for Theorem ProvingMatthias Baaz, Agata Ciabattoni, Christian G. Fermüller. 201-215 [doi]
- Unification in a Description Logic with Transitive Closure of RolesFranz Baader, Ralf Küsters. 217-232 [doi]
- Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph DescriptionsGuy Perrier. 233-248 [doi]
- Coherence and Transitivity in Coercive SubtypingYong Luo, Zhaohui Luo. 249-265 [doi]
- A Type-Theoretic Approach to Induction with Higher-Order EncodingsCarsten Schürmann. 266-281 [doi]
- Analysis of Polymorphically Typed Logic Programs Using ACI-UnificationJan-Georg Smaus. 282-298 [doi]
- Model Generation with Boolean ConstraintsMiyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa. 299-308 [doi]
- First-Order Atom Definitions ExtendedBijan Afshordel, Thomas Hillenbrand, Christoph Weidenbach. 309-319 [doi]
- Automated Proof Support for Interval LogicsThomas Marthedal Rasmussen. 320-329 [doi]
- The Functions Provable by First Order AbstractionDaniel Leivant. 330-346 [doi]
- A Local System for Classical LogicKai Brünnler, Alwen Fernanto Tiu. 347-361 [doi]
- Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean FormulaeJussi Rintanen. 362-376 [doi]
- Permutation Problems and Channelling ConstraintsToby Walsh. 377-391 [doi]
- Simplifying Binary Propositional Theories into Connected Components Twice as FastAlvaro del Val. 392-406 [doi]
- Reasoning about Evolving Nonmonotonic Knowledge BasesThomas Eiter, Michael Fink, Giuliana Sabbatini, Hans Tompits. 407-421 [doi]
- Efficient Computation of the Well-Founded Model Using Update PropagationAndreas Behrend. 422-437 [doi]
- Indexed Categories and Bottom-Up Semantics of Logic ProgramsGianluca Amato, James Lipton. 438-454 [doi]
- Functional Logic Programming with Failure: A Set-Oriented ViewFrancisco Javier López-Fraguas, Jaime Sánchez-Hernández. 455-469 [doi]
- Operational Semantics for Fixed-Point Logics on Constraint DatabasesStephan Kreutzer. 470-484 [doi]
- Efficient Negation Using Abstract InterpretationSusana Muñoz-Hernández, Juan José Moreno-Navarro, Manuel V. Hermenegildo. 485-494 [doi]
- Certifying Synchrony for FreeSylvain Boulmé, Grégoire Hamon. 495-506 [doi]
- A Computer Environment for Writing Ordinary Mathematical ProofsDavid McMath, Marianna Rozenfeld, Richard Sommer. 507-516 [doi]
- On Termination of Meta-ProgramsAlexander Serebrenik, Danny De Schreye. 517-530 [doi]
- A Monotonic Higher-Order Semantic Path OrderingCristina Borralleras, Albert Rubio. 531-547 [doi]
- The Elog Web Extraction LanguageRobert Baumgartner, Sergio Flesca, Georg Gottlob. 548-560 [doi]
- Census Data Repair: a Challenging Application of Disjunctive Logic ProgrammingEnrico Franconi, Antonio Laureti Palma, Nicola Leone, Simona Perri, Francesco Scarcello. 561-578 [doi]
- Boolean Functions for Finite-Tree DependenciesRoberto Bagnara, Enea Zaffanella, Roberta Gori, Patricia M. Hill. 579-594 [doi]
- How to Transform an Analyzer into a VerifierMarco Comini, Roberta Gori, Giorgio Levi. 595-609 [doi]
- Andorra Model Revised: Introducing Nested Domain Variables and a Targeted SearchRong Yang, Steve Gregory. 610-623 [doi]
- Coherent Composition of Distributed Knowledge-Bases Through AbductionOfer Arieli, Bert Van Nuffelen, Marc Denecker, Maurice Bruynooghe. 624-638 [doi]
- Tableaux for Reasoning About Atomic UpdatesChristian G. Fermüller, Georg Moser, Richard Zach. 639-653 [doi]
- Inference of Termination Conditions for Numerical Loops in PrologAlexander Serebrenik, Danny De Schreye. 654-668 [doi]
- Termination of Rewriting With Strategy AnnotationsSalvador Lucas. 669-684 [doi]
- Inferring Termination Conditions for Logic Programs Using Backwards AnalysisSamir Genaim, Michael Codish. 685-694 [doi]
- Reachability Analysis of Term Rewriting Systems with TimbukThomas Genet, Valérie Viet Triem Tong. 695-706 [doi]
- Binding-Time Annotations Without Binding-Time AnalysisWim Vanhoof, Maurice Bruynooghe. 707-722 [doi]
- Concept Formation via Proof Planning FailureRaul Monroy. 723-736 [doi]