Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Amine Chaieb, Tobias Nipkow |
Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio |
Recursive Path Orderings Can Also Be Incremental. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Calvin Kai Fan Tang, Eugenia Ternovska |
Model Checking Abstract State Machines with Answer Set Programming. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Elaine Pimentel, Dale Miller 0001 |
On the Specification of Sequent Systems. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Dix, Wolfgang Faber 0001, V. S. Subrahmanian |
The Relationship Between Reasoning About Privacy and Default Logics. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Fritz |
Concepts of Automata Construction from LTL. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Beckert, Kerry Trentelman |
Second-Order Principles in Specification Languages for Object-Oriented Programs. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Christian Anger, Martin Gebser, Thomas Linke, André Neumann, Torsten Schaub |
The nomore++ Approach to Answer Set Solving. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Walther, Stephan Schweitzer |
Reasoning About Incompletely Defined Programs. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Henning Christiansen 0001, Davide Martinenghi |
Incremental Integrity Checking: Limitations and Possibilities. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Yao Wu, Enrico Pontelli, Desh Ranjan |
Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi |
Treewidth in Verification: Local vs. Global. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Matthias M. Hölzl, John N. Crossley |
Disjunctive Constraint Lambda Calculi. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Marc Bezem, Thierry Coquand |
Automating Coherent Logic. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang |
Functional Correctness Proofs of Encryption Algorithms. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Laura Giordano 0001, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato |
Analytic Tableaux for KLM Preferential and Cumulative Logics. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Larchey-Wendling |
Bounding Resource Consumption with Gödel-Dummett Logics. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Wieslaw Szwast, Lidia Tendera |
On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
computational complexity, transitivity, decision problem, guarded fragment, finite model |
1 | Laura Bozzelli, Aniello Murano, Adriano Peron |
Pushdown Module Checking. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi |
Zap: Automated Theorem Proving for Software Analysis. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Sylvie Coste-Marquis, Caroline Devred, Pierre Marquis |
Inference from Controversial Arguments. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec |
Strong Normalization of the Dual Classical Sequent Calculus. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Maarten Mariën, Rudradeb Mitra, Marc Denecker, Maurice Bruynooghe |
Satisfiability Checking for PC(ID). |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Vladimir Aleksic, Anatoli Degtyarev |
Regular Derivations in Basic Superposition-Based Calculi. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Nachum Dershowitz |
The Four Sons of Penrose. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Allen Van Gelder |
Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Florina Piroi, Temur Kutsia |
The Theorema Environment for Interactive Proof Development. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Dal Palù, Agostino Dovier, Enrico Pontelli |
A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Chao Wang 0001, Franjo Ivancic, Malay K. Ganai, Aarti Gupta |
Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Robert Nieuwenhuis, Albert Oliveras |
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Douglas B. Lenat |
Scaling Up: Computers vs. Common Sense. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Daum 0001, Stefan Maus, Norbert Schirmer, Mohamed Nassim Seghir |
Integration of a Software Model Checker into Isabelle. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Mikhail Sheremet, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev |
Comparative Similarity, Tree Automata, and Diophantine Equations. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Didier Galmiche, Daniel Méry |
Characterizing Provability in . |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Haiou Shen, Hantao Zhang 0001 |
Another Complete Local Search Method for SAT. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Salvador Lucas, José Meseguer 0001 |
Termination of Fair Computations in Term Rewriting. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
fairness, program analysis, Concurrent programming, termination, term rewriting |
1 | Hitoshi Ohsaki, Jean-Marc Talbot, Sophie Tison, Yves Roos |
Monotone AC-Tree Automata. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
equational tree automata, complexity, decidability, closure properties |
1 | David A. Basin, Sebastian Mödersheim, Luca Viganò 0001 |
Algebraic Intruder Deductions. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Mehdi Dastani, Guido Governatori, Antonino Rotolo, Leendert W. N. van der Torre |
Programming Cognitive Agents in Defeasible Logic. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Baaz, Rosalie Iemhoff |
On Interpolation in Existence Logics. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
existence predicate, Gentzen calculus, Beth definability, truth-value logics, Gödel logics, Scott logics, interpolation, cut-elimination, Intuitionistic logic, Kripke models, Skolemization |
1 | Angelo Montanari, Alberto Policriti, Nicola Vitacolonna |
An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Annabelle McIver, Tjark Weber |
Towards Automated Proof Support for Probabilistic Distributed Systems. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Davy Van Nieuwenborgh, Stijn Heymans, Dirk Vermeir |
Weighted Answer Sets and Applications in Intelligence Analysis. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | M. Jamshid Bagherzadeh, S. Arun-Kumar |
Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
proof method, multi-agent systems, resolution, belief revision, multi-modal logic |
1 | Vilhelm Dahllöf |
Applications of General Exact Satisfiability in Propositional Logic Modelling. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Benjamin Aminof, Thomas Ball, Orna Kupferman |
Reasoning About Systems with Transition Fairness. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
Abstract DPLL and Abstract DPLL Modulo Theories. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr |
Cut-Elimination: Experiments with CERES. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride |
Knowledge-Based Synthesis of Distributed Systems Using Event Structures. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Dietmar Berwanger, Erich Grädel |
Entanglement - A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber |
Can a Higher-Order and a First-Order Theorem Prover Cooperate?. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Ullrich Hustadt, Boris Motik, Ulrike Sattler |
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Jerzy Marcinkowski, Jan Otop, Grzegorz Stelmaszek |
On a Semantic Subsumption Test. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Linke, Vladimir Sarsakov |
Suitable Graphs for Answer Set Programming. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Eiter, Giovambattista Ianni, Roman Schindlauer, Hans Tompits |
Nonmonotonic Description Logic Programs: Implementation and Experiments. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Nathan Whitehead, Martín Abadi |
BCiC: A System for Code Authentication and Verification. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Lennart Beringer, Martin Hofmann 0001, Alberto Momigliano, Olha Shkaravska |
Automatic Certification of Heap Consumption. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Norbert Schirmer |
A Verification Environment for Sequential Imperative Programs in Isabelle/HOL. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Markus Müller-Olm, Helmut Seidl |
A Generic Framework for Interprocedural Analyses of Numerical Properties. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Pablo López, Jeff Polakow |
Implementing Efficient Resource Management for Linear Logic Programming. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Christopher Hardin |
How the Location of * Influences Complexity in Kleene Algebra with Tests. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Baaz, Alexander Leitsch |
CERES in Many-Valued Logics. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Giesl, René Thiemann, Peter Schneider-Kamp |
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Helmut Seidl, Kumar Neeraj Verma |
Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Marco Benedetti |
Evaluating QBFs via Symbolic Skolemization. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Paul Hankes Drielsma, Sebastian Mödersheim, Luca Viganò 0001 |
A Formalization of Off-Line Guessing for Security Protocol Analysis. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Pascal Fontaine, Silvio Ranise, Calogero G. Zarba |
Combining Lists with Non-stably Infinite Theories. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Roberto Di Cosmo, Thomas Dufour |
The Equational Theory of < N, 0, 1, +, ×, uparrow > Is Decidable, but Not Finitely Axiomatisable. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Flávio L. C. de Moura, Fairouz Kamareddine, Mauricio Ayala-Rincón |
Second-Order Matching via Explicit Substitutions. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
Higher-Order Unification, Second-Order Matching, Explicit Substitutions |
1 | Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa |
Abstract Model Generation for Preprocessing Clause Sets. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Igor Walukiewicz |
How to Fix It: Using Fixpoints in Different Contexts. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Gustav Nordh |
A Trichotomy in the Complexity of Propositional Circumscription. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Elvira Albert, Germán Puebla, Manuel V. Hermenegildo |
Abstraction-Carrying Code. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, Sungwoo Park |
The Inverse Method for the Logic of Bunched Implications. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Lucas Bordeaux, Marco Cadoli, Toni Mancini |
Exploiting Fixable, Removable, and Implied Values in Constraint Satisfaction Problems. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Carlos Areces, Daniel Gorín |
Ordered Resolution with Selection for H(@). |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Walther, Stephan Schweitzer |
Automated Termination Analysis for Incompletely Defined Programs. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Agata Ciabattoni, Christian G. Fermüller, George Metcalfe |
Uniform Rules and Dialogue Games for Fuzzy Logics. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Quoc Bao Vo, Abhaya C. Nayak, Norman Y. Foo |
A Syntax-Based Approach to Reasoning about Actions and Events. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Ciaffaglione, Luigi Liquori, Marino Miculan |
Imperative Object-Based Calculi in Co-inductive Type Theories. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Dietrich Kuske |
Is Cantor's Theorem Automatic? |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Matthias Baaz, Christian G. Fermüller |
A Translation Characterizing the Constructive Content of Classical Theories. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Furio Honsell, Marina Lenisa, Rekha Redamalla |
Strict Geometry of Interaction Graph Models. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
(linear) graph model, traced monoidal category, weak linear category, categorical geometry of interaction |
1 | Paola Bruscoli, Alessio Guglielmi |
On Structuring Proof Search for First Order Linear Logic. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Robert Nieuwenhuis, Albert Oliveras |
Congruence Closure with Integer Offsets. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Markus Lohrey |
Automatic Structures of Bounded Degree. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
A Formal Proof of Dickson's Lemma in ACL2. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Walther, Stephan Schweitzer |
A Machine-Verified Code Generator. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Franz Baader, Jan Hladik, Carsten Lutz, Frank Wolter |
From Tableaux to Automata for Description Logics. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Margarita V. Korovina |
Gandy's Theorem for Abstract Structures without the Equality Test. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Serikzhan A. Badaev |
Computable Numberings. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Wilke |
Minimizing Automata on Infinite Words. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Dietmar Berwanger, Erich Grädel, Stephan Kreutzer |
Once upon a Time in a West - Determinacy, Definability, and Complexity of Path Games. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Kumar Neeraj Verma |
On Closure under Complementation of Equational Tree Automata for Theories Extending AC. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Sebastian Brandt 0001, Anni-Yasmin Turhan, Ralf Küsters |
Extensions of Non-standard Inferences to Descriptions Logics with Transitive Roles. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Heinemann |
Extended Canonicity of Certain Topological Properties of Set Spaces. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
modal logic of subset spaces, rules in modal languages with names, topological reasoning, canonicity |
1 | Moshe Y. Vardi, Andrei Voronkov (eds.) |
Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Beierle, Gabriele Kern-Isberner |
A Logical Study on Qualitative Default Reasoning with Probabilities. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Davy Van Nieuwenborgh, Dirk Vermeir |
Ordered Diagnosis. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Silvio Ghilardi, Luigi Santocanale |
Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics. |
LPAR |
2003 |
DBLP DOI BibTeX RDF |
|