Computer Science Logic
Springer Berlin (Verlag)
978-3-540-23024-3 (ISBN)
Invited Lectures.- Notions of Average-Case Complexity for Random 3-SAT.- Abstract Interpretation of Proofs: Classical Propositional Calculus.- Applications of Craig Interpolation to Model Checking.- Bindings, Mobility of Bindings, and the ?-Quantifier: An Abstract.- My (Un)Favourite Things.- Regular Papers.- On Nash Equilibria in Stochastic Games.- A Bounding Quantifier.- Parity and Exploration Games on Infinite Graphs.- Integrating Equational Reasoning into Instantiation-Based Theorem Proving.- Goal-Directed Methods for ?ukasiewicz Logic.- A General Theorem on Termination of Rewriting.- Predicate Transformers and Linear Logic: Yet Another Denotational Model.- Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity.- On Proof Nets for Multiplicative Linear Logic with Units.- The Boundary Between Decidability and Undecidability for Transitive-Closure Logics.- Game-Based Notions of Locality Over Finite Models.- Fixed Points of Type Constructors and Primitive Recursion.- On the Building of Affine Retractions.- Higher-Order Matching in the Linear ?-calculus with Pairing.- A Dependent Type Theory with Names and Binding.- Towards Mechanized Program Verification with Separation Logic.- A Functional Scenario for Bytecode Verification of Resource Bounds.- Proving Abstract Non-interference.- Intuitionistic LTL and a New Characterization of Safety and Liveness.- Moving in a Crumbling Network: The Balanced Case.- Parameterized Model Checking of Ring-Based Message Passing Systems.- A Third-Order Bounded Arithmetic Theory for PSPACE.- Provably Total Primitive Recursive Functions: Theories with Induction.- Logical Characterizations of PSPACE.- The Logic of the Partial ?-Calculus with Equality.- Complete Lax Logical Relations for Cryptographic Lambda-Calculi.-Subtyping Union Types.- Pfaffian Hybrid Systems.- Axioms for Delimited Continuations in the CPS Hierarchy.- Set Constraints on Regular Terms.- Unsound Theorem Proving.- A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation.- Automated Generation of Analytic Calculi for Logics with Linearity.
Erscheint lt. Verlag | 2.9.2004 |
---|---|
Reihe/Serie | Lecture Notes in Computer Science |
Zusatzinfo | XI, 522 p. |
Verlagsort | Berlin |
Sprache | englisch |
Maße | 155 x 235 mm |
Gewicht | 840 g |
Themenwelt | Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge |
Informatik ► Theorie / Studium ► Compilerbau | |
Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik | |
Schlagworte | 3-SAT • AI logics • Calculus • Classical Logic • Complexity • Computer Science Logic • Erfüllbarkeitsproblem der Aussagenlogik • formale Sprachen • Higher Order Logic • inference • Linear Logic • Logic • Logical calculi • Mathematical Logic • Mathematische Logik • Model Checking • nonclassical logic • Programming Logic • Proof theory • proving • Term Rewriting • theorem proving • verification |
ISBN-10 | 3-540-23024-6 / 3540230246 |
ISBN-13 | 978-3-540-23024-3 / 9783540230243 |
Zustand | Neuware |
Haben Sie eine Frage zum Produkt? |
aus dem Bereich