Category:Logic in computer science

Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains:

1. Those investigations into logic that are guided by applications in computer science. For example:
   • Rewriting systems, Combinatory logic and Abstract interpretation;
2. Fundamental concepts in computer science that are naturally expressible in logical form. For example:
   • Type theory (used in type systems), Formal semantics of programming languages, Hoare logic, and Logic programming;
3. Applications of fundamental concepts derived from the theory of computation that cast light on questions of pure logic. For example:
   • Curry-Howard correspondence and Game semantics;
4. Tools for logicians considered as applied computer science. For example:
   • Automated theorem proving and Model checking.

See also Category: Finite model theory.

Subcategories

This category has the following 14 subcategories, out of 14 total.

A [+] Automated theorem proving‎ (2 C, 29 P) C [+] Categorical logic‎ (1 C, 5 P) [+] Combinatory logic‎ (1 C, 8 P) D [+] Denotational semantics‎ (1 C, 7 P) G [×] Logic gates‎ (33 P)

L [×] Logic conferences‎ (11 P) [×] Logic families‎ (33 P) [+] Logic programming‎ (6 C, 42 P) [+] Logical calculi‎ (4 C, 31 P) P [×] Program logic‎ (3 P)

P cont. [+] Programming language semantics‎ (2 C, 14 P) T [×] Temporal logic‎ (11 P) [+] Type theory‎ (3 C, 93 P) Z [×] Z notation‎ (17 P)

Pages in category "Logic in computer science"

The following 85 pages are in this category, out of 85 total. This list may not reflect recent changes (learn more).

A Abstract rewriting system Alternating-time Temporal Logic Assertion (computing) Automated reasoning Axiomatic semantics B Backward chaining Bisimulation Boolean circuit Boolean satisfiability problem Bunched logic C Circuit minimization Combinational logic Combinatory logic Compcert Computability logic Computation tree logic CTL* Curry–Howard correspondence D Decidable sublanguages of set theory Denotational semantics Dynamic logic (modal logic) E Event calculus F Fluent (artificial intelligence) Formal verification Forward chaining Frege system Functional completeness Combs method Fuzzy logic

G Game semantics Geometry of interaction H Hennessy–Milner logic Herbrand Award HOL (proof assistant) Horn clause Horn-satisfiability I IEEE Symposium on Logic in Computer Science Intuitionistic logic Intuitionistic type theory J Journal of Automated Reasoning Journal of Logic and Computation K Karnaugh map Knowledge Interchange Format L Logic for Computable Functions Logical framework Logical Methods in Computer Science M User:Madhurbajpai/Formal Verification Maximum satisfiability problem Model elimination Multi-Agent Programming Contest Noise-based logic N Normalization property (abstract rewriting) O OBJ (programming language) Operational semantics Ordered Weighted Averaging (OWA) Aggregation Operators P Peano axioms Perceptual Computing Postcondition

P cont. Precondition Preferential entailment Presburger arithmetic Proof complexity Propositional proof system Q Q zero R Race condition Racetrack problem User:Rahulbhalerao001`/Formal verification Rewriting Runtime verification S Satisfiability Modulo Theories Semantics of programming languages Separation logic Star-free language State space enumeration Structural induction Stuttering equivalence T Topological computing Truth bit Twelf Type-2 fuzzy sets and systems Typed lambda calculus U Undecidable problem W WalkSAT Weakest precondition Λ ΛProlog