Logic in Computer Science

DOI10.1017/CBO9780511810275zbMath1073.68001OpenAlexW4251228600MaRDI QIDQ4830107

No author found.

Publication date: 3 December 2004

Full work available at URL: https://doi.org/10.1017/cbo9780511810275

modal logic textbook propositional logic Boolean functions model checking natural deduction multiagent systems binary decision diagrams predicate logic program verification SAT solver data structure logic of knowledge object modeling contract-programming paradigm

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Logic in artificial intelligence (68T27) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Completeness for recursive procedures in separation logic, Diagnosability of delay-deadline failures in fair real time discrete event models, Indexed and fibered structures for partial and total correctness assertions, Specification and Verification of Multi-Agent Systems, Quantified epistemic logics for reasoning about knowledge in multi-agent systems, Linear temporal logic vehicle routing with applications to multi-UAV mission planning, The Complexity of Linear-Time Temporal Logic Model Repair, Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method, Practical verification of multi-agent systems against \textsc{Slk} specifications, Undecidability of QLTL and QCTL with two variables and one monadic predicate letter, Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization, Complexity of finite-variable fragments of propositional temporal and modal logics of computation, Modal operators on pseudo-BE algebras, 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, Computational logic: its origins and applications, A formalism to specify unambiguous instructions inspired by Mīmāṁsā in computational settings, Yet Another Kind of Rough Sets Induced by Coverings, Formal modeling and verification for MVB, Model Checking of Robot Gathering, A process calculus for privacy-preserving protocols in location-based service systems, Knowledge and Games in Modal Semirings, An accessible verification environment for UML models of services, Verifying the consistency of web-based technical documentations, Modelling mutual exclusion in a process algebra with time-outs, Global view on reactivity: switch graphs and their logics, Characterizing and extending answer set semantics using possibility theory, Probabilistic (logic) programming concepts, Are bundles good deals for first-order modal logic?, A Spatial Logic for Simplicial Models, Keeping logic in the trivium of computer science: a teaching perspective, Synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction, On the computation of counterexamples in compositional nonblocking verification, Model checking the observational determinism security property using PROMELA and SPIN, Typed context awareness ambient calculus for pervasive applications, Formalizing a hierarchical file system, Kripke modelling and verification of temporal specifications of a multiple UAV system, A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes, Comparative Analysis of Statistical Model Checking Tools, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Dual and axiomatic systems for constructive S4, a formally verified equivalence, Linear temporal logic symbolic model checking, Temporal normal form for Linear Temporal Logic formulae1, Keeping calm in the face of change. Towards optimisation of FRP by reasoning about change, Formalizing a Hierarchical File System, Verification of asynchronous systems with an unspecified component, Minimal refinements of specifications in modal and temporal logics, Safe autonomy under perception uncertainty using chance-constrained temporal logic, Synthesis of obfuscation policies to ensure privacy and utility, Parallelizing SMT solving: lazy decomposition and conciliation, A resolution calculus for the branching-time temporal logic CTL, Construction of parametric barrier functions for dynamical systems using interval analysis, Reasoning about truth in first-order logic, Fair multi-party contract signing using private contract signatures, The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4, Performability assessment by model checking of Markov reward models, Hoare logic-based genetic programming, Minimal refinements of specifications in modal and temporal logics, A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus, A Refined Resolution Calculus for CTL, The RISC ProofNavigator: a proving assistant for program verification in the classroom, Automatic proofs of memory deallocation for a Whiley-to-C compiler, Merging Procedural and Declarative Proof, Axiomatic and dual systems for constructive necessity, a formally verified equivalence, 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, A framework for compositional nonblocking verification of extended finite-state machines