Logic in Computer Science
From MaRDI portal
Publication:4830107
DOI10.1017/CBO9780511810275zbMATH Open1073.68001OpenAlexW4251228600MaRDI QIDQ4830107FDOQ4830107
Authors:
Publication date: 3 December 2004
Full work available at URL: https://doi.org/10.1017/cbo9780511810275
Recommendations
data structuremodel checkingmodal logicnatural deductiontextbookBoolean functionsmultiagent systemspredicate logicprogram verificationpropositional logicSAT solverbinary decision diagramslogic of knowledgeobject modelingcontract-programming paradigm
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in artificial intelligence (68T27) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01)
Cited In (81)
- Minimal refinements of specifications in modal and temporal logics
- Minimal refinements of specifications in modal and temporal logics
- Formalizing a hierarchical file system
- Modal operators on pseudo-BE algebras
- Modelling mutual exclusion in a process algebra with time-outs
- Temporal normal form for linear temporal logic formulae
- Indexed and fibered structures for partial and total correctness assertions
- Describing the what and why of students' difficulties in Boolean logic
- Title not available (Why is that?)
- Representation theorems in computer science. A treatment in logic engineering
- On the benefits of knowledge compilation for feature-model analyses
- Tractable representations for Boolean functional synthesis
- Formalising the double-pushout approach to graph transformation
- Are bundles good deals for first-order modal logic?
- Title not available (Why is that?)
- Generalized qualitative spatio-temporal reasoning: complexity and tableau method
- Thinking programs. Logical modeling and reasoning about languages, data, computations, and executions
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- An environment for specifying and model checking mobile ring robot algorithms
- A Spatial Logic for Simplicial Models
- Model checking of robot gathering
- NOTIONAL LOGIC OF SYSTEMS
- A framework for compositional nonblocking verification of extended finite-state machines
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence
- A process calculus for privacy-preserving protocols in location-based service systems
- Abstraction and approximation in fuzzy temporal logics and models
- Machine learning for first-order theorem proving
- Verification of asynchronous systems with an unspecified component
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus
- Completeness for recursive procedures in separation logic
- Characterizing and extending answer set semantics using possibility theory
- Safe autonomy under perception uncertainty using chance-constrained temporal logic
- Merging Procedural and Declarative Proof
- A Refined Resolution Calculus for CTL
- Parallelizing SMT solving: lazy decomposition and conciliation
- 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
- The Complexity of Linear-Time Temporal Logic Model Repair
- Formalized proof systems for propositional logic
- Title not available (Why is that?)
- A formalism to specify unambiguous instructions inspired by Mīmāṁsā in computational settings
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
- 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
- An accessible verification environment for UML models of services
- Verifying the consistency of web-based technical documentations
- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization
- Synthesis of obfuscation policies to ensure privacy and utility
- Linear temporal logic symbolic model checking
- Probabilistic (logic) programming concepts
- Performability assessment by model checking of Markov reward models
- Knowledge and Games in Modal Semirings
- Global view on reactivity: switch graphs and their logics
- Model checking the observational determinism security property using PROMELA and SPIN
- A doctrinal approach to modal/temporal Heyting logic and non-determinism in processes
- Specification and Verification of Multi-Agent Systems
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Fair multi-party contract signing using private contract signatures
- Comparative analysis of statistical model checking tools
- Complexity of finite-variable fragments of propositional temporal and modal logics of computation
- Synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction
- Diagnosability of delay-deadline failures in fair real time discrete event models
- Computational logic: its origins and applications
- Hoare logic-based genetic programming
- Formal modeling and verification for MVB
- Quantified epistemic logics for reasoning about knowledge in multi-agent systems
- Title not available (Why is that?)
- Yet another kind of rough sets induced by coverings
- Keeping calm in the face of change. Towards optimisation of FRP by reasoning about change
- Keeping logic in the trivium of computer science: a teaching perspective
- A resolution calculus for the branching-time temporal logic CTL
- On the computation of counterexamples in compositional nonblocking verification
- Linear temporal logic vehicle routing with applications to multi-UAV mission planning
- Practical verification of multi-agent systems against \textsc{Slk} specifications
- Construction of parametric barrier functions for dynamical systems using interval analysis
- Reasoning about truth in first-order logic
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
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)
