Logic in Computer Science
From MaRDI portal
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)
Recommendations
Cited in
(86)- 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
- 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)
