Logic in Computer Science
binary decision diagramsBoolean functionscontract-programming paradigmdata structurelogic of knowledgemodal logicmodel checkingmultiagent systemsnatural deductionobject modelingpredicate logicprogram verificationpropositional logicSAT solvertextbook
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in artificial intelligence (68T27)
[For a review of the first edition (2000) see Zbl 0955.68001.] This book provides an elegant introduction to formal reasoning that is relevant to computation science. This second edition improves the first one with extra and expanded sections on temporal logic model checking, SAT solvers, second-order logic, the Alloy specification language, and programming by contract. The material is up-to-date and practical and is organized as follows: Chapter 1 is devoted to natural deduction techniques and the design, correctness and complexity of a SAT solver for full propositional classical logic. Chapter 2 deals with several issues about predicate logic: undecidability, expressiveness, etc. Also, an object modelling language, Alloy, is defined. Alloy is an automatic (model based) property-verification approach. This tool finds models which form counterexamples to assertions made by the user. In Chapter 3, a full exposition of a verification method of model checking is introduced. Model checking is an important tool on the design and debugging of a system and it is based on temporal logic. In Chapter 4, verification methods for sequential programms running on a simple process are introduced. This chapter contains a new section on the contract-programming paradigm of verifying program correctness. Chapter 5 is devoted to a logic engineering approach by using modal logic. The main case study is the logic of knowledge in multiagent systems. Finally, Chapter 6 concerns Boolean functions, a descriptive formalism for many hardware and software systems such as asynchronous circuits and reactive systems.
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- Practical verification of multi-agent systems against \textsc{Slk} specifications
- Keeping logic in the trivium of computer science: a teaching perspective
- Verification of asynchronous systems with an unspecified component
- Parallelizing SMT solving: lazy decomposition and conciliation
- Global view on reactivity: switch graphs and their logics
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Complexity of finite-variable fragments of propositional temporal and modal logics of computation
- Why there is no general solution to the problem of software verification
- A two-level approach based on model checking to support architecture conformance checking
- A formalism to specify unambiguous instructions inspired by Mīmāṁsā in computational settings
- Synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction
- On the computation of counterexamples in compositional nonblocking verification
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- Reasoning about truth in first-order logic
- Machine learning for first-order theorem proving
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
- Abstraction and approximation in fuzzy temporal logics and models
- Fair multi-party contract signing using private contract signatures
- A framework for compositional nonblocking verification of extended finite-state machines
- A process calculus for privacy-preserving protocols in location-based service systems
- Completeness for recursive procedures in separation logic
- Linear temporal logic vehicle routing with applications to multi-UAV mission planning
- Comparative analysis of statistical model checking tools
- Temporal normal form for linear temporal logic formulae
- Formalizing a hierarchical file system
- Diagnosability of delay-deadline failures in fair real time discrete event models
- Specification and Verification of Multi-Agent Systems
- Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization
- Model checking of robot gathering
- A simple functional presentation and an inductive correctness proof of the Horn algorithm
- Generalized qualitative spatio-temporal reasoning: complexity and tableau method
- Knowledge and Games in Modal Semirings
- Merging Procedural and Declarative Proof
- Formal modeling and verification for MVB
- Formalizing a hierarchical file system
- Kripke modelling and verification of temporal specifications of a multiple UAV system
- Computational logic: its origins and applications
- Characterizing and extending answer set semantics using possibility theory
- A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes
- Linear temporal logic symbolic model checking
- NOTIONAL LOGIC OF SYSTEMS
- scientific article; zbMATH DE number 1446599 (Why is no real title available?)
- Thinking programs. Logical modeling and reasoning about languages, data, computations, and executions
- scientific article; zbMATH DE number 7453963 (Why is no real title available?)
- The Complexity of Linear-Time Temporal Logic Model Repair
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
- Yet another kind of rough sets induced by coverings
- Construction of parametric barrier functions for dynamical systems using interval analysis
- A Refined Resolution Calculus for CTL
- Representation theorems in computer science. A treatment in logic engineering
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Describing the what and why of students' difficulties in Boolean logic
- A resolution calculus for the branching-time temporal logic CTL
- Hoare logic-based genetic programming
- A linear translation from CTL^* to the first-order modal -calculus
- Modal operators on pseudo-BE algebras
- Indexed and fibered structures for partial and total correctness assertions
- Minimal refinements of specifications in modal and temporal logics
- Minimal refinements of specifications in modal and temporal logics
- Modelling mutual exclusion in a process algebra with time-outs
- Formalized proof systems for propositional logic
- Are bundles good deals for first-order modal logic?
- scientific article; zbMATH DE number 7809761 (Why is no real title available?)
- A Spatial Logic for Simplicial Models
- An accessible verification environment for UML models of services
- Verifying the consistency of web-based technical documentations
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- An environment for specifying and model checking mobile ring robot algorithms
- Keeping calm in the face of change. Towards optimisation of FRP by reasoning about change
- On the benefits of knowledge compilation for feature-model analyses
- Tractable representations for Boolean functional synthesis
- Formalising the double-pushout approach to graph transformation
- Safe autonomy under perception uncertainty using chance-constrained temporal logic
- Synthesis of obfuscation policies to ensure privacy and utility
- Refined tableau systems for some modal logics of confluence
- Two-dimensional Kripke semantics i: presheaves
- A Mīmāṃsā inspired framework towards temporal reasoning in large language models
- Some uses of modal semirings
- Day algebras
- Multiple interdependent simple temporal networks with uncertainty: a semi-decentralized multi-agent model with shared control of activity durations
- Propositional Proof Systems
- Quantified epistemic logics for reasoning about knowledge in multi-agent systems
- Probabilistic (logic) programming concepts
- Model checking the observational determinism security property using PROMELA and SPIN
- Typed context awareness ambient calculus for pervasive applications
- Performability assessment by model checking of Markov reward models
This page was built for publication: Logic in Computer Science
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4830107)
