FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
GLOBAL TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

#
#SAT
#SMT(BV)
#SMT(LA)
2
2-CNF
A
A-infinity-(co)algebras
abductive reasoning
Abella
ABNF
Absolute Correctness
Abstract Interpretation
abstract recursion theory
abstract state machine
Abstract State Machines
Abstract syntax
abstract winning condition
Abstraction
abstraction learning
Abstraction Refinement
abstraction-refinement
accumulated weight constraints
Ackermann's Lemma
ACL2
action language
Active Objects
Actor
actors
Actual Cause
ACUI
Ada programming
adaptive
additive monad
adequate numeral system
(ITRS)
adjoint logic
adjoint model
adjunction
Adjunctions
admissibility
admissible rules
affine term
Agda
agent policies
agent programming
agents
Aggregates
aggregations in logic programming
AI Safety
air traffic surveillance systems
Alarm ranking
Algebra
algebra in type theory
algebraic confluence
Algebraic crossover operators
algebraic effects
Algebraic evolutionary computation
algebraic extensions
Algebraic Geometry
algebraic proof systems
algebraic structures
algorithm
Algorithm selection
algorithm substitution attacks
algorithmic complexity
algorithms
all maximal clique partitions in a graph
allegories
alloy
Almost Full relations
Almost-sure winning
alpha-equivalence
Alternating Automata
Alternating time
Alternating-time Temporal Logic
AMBA AHB
anaphora
Android Applications
Android back stack
Android stack systems
Animation
annotation
answer set
answer set computation
Answer Set Programming
Answer Set Programming Extensions
Anti-unification
Apache Spark
Application
applicative bisimulation distance
applicative first-order logic
applicative functor
applicative simulation distance
applied lambda-calculus
Apprenticeship Learning
Approximable Mappings
approximate circuits
approximate counting
approximate equivalence checking
Approximate inference
approximate partial order reduction
Approximate synthesis
Approximation
Approximation Fixpoint Theory
approximation theorem
architecture
Arithmetic
arithmetic circuits
Armstrong relation
Array
Arrays
arrow
Artificial Intelligence
ASMETA
ASN.1
ASP
ASP systems
ASPIDE
Assertions
Associative operad
assumptions refinement
Asynchronous
Asynchronous Games
Atom tracing
atom variables
Atomic flows
Atomic Formula
ATP
Attack patterns
attack trees
attacker knowledge
Attempto Controlled English
attribute-based access control
Authentication
auto-generated code
autocorrelation
automata
automata learning
Automata over infinite words
automata theory
Automata with counters
Automated Algebraic Reasonings
automated complexity analysis
Automated configuration
Automated digital control
automated guided vehicle routing
automated reasoning
automated reasonning
automated theorem proving
automated trading systems
Automated verification
automatic algorithm configuration
Automatic Program Verification
Automatic Proof checking
Automatic Verification
automation
Automaton State
automotive
Automotive case study
Autonomous
Autonomous automotive
Autonomous Driving
Autonomous system
Autonomous vehicle
autonomous vehicles
avatar
avionics systems
Axiom Pinpointing
axiomatic domain theory
Axiomatic Method
axiomatization
axioms
B
B combinator
B+ trees
back-and-forth equivalences
backdoor
backdoors
backtracking
Backus FP
Backward exploration ·
backwards analysis
Bar inductive predicates
barcan formulas
Barendregt's Variable Convention
barrier certificates
Basis Reduction
Bayesian inference
Bayesian learning
Bayesian network
BayesianInference
BDD
Behavioural equivalence
Behavioural metrics
Belenios
Belief Function Theory
belief merging
Belief networks
benchmark
Benchmarking
beta reduction
Beth models
Betweenness Centrality
Bi-directional Grammars
bi-intuitionistic logic
bicategories
Bidding games
Biform theories
BiLSTM
Bimonad
binarized neural network
binarized neural networks
Binary Analysis
Binary Encoding
binary search tree
binder mobility
Binders
Binding operations
Bioinformatics
bisimulation
bit-blasting
Bit-vectors
Bitcoin
Bitvectors
black-box optimization
BLESS
Blockchain
blocked clauses
bobs-only
boolean algebra
Boolean Functional synthesis
Boolean games
Boolean polynomials
Boolean Satisfiability
Boolean-valued models
Boot code
bottom-up
Bounded
bounded arithmetic
Bounded expansion
bounded model checking
bounded model-checking
bounded synthesis
bounds on leakage
Braidings
branching programs
broadcast communication
Brzozowski derivatives
Buchberger algorithm
Buchi Automaton
Bug Finding
bug finding tool
Bunched Implications Logic
Business Process Model
Böhm trees
Büchi Automaton
C
C code
C Programming Language
cache coherence protocols
Cached Address Translation
CakeML
calculational method
Calculational proof
calculus of structures
call by push value
call by value
call-by-name
call-by-need evaluation
call-by-push value
call-by-push-value
call-by-value
CAMUS
car assembly operations
Cardinality Constraint
cardinality encodings
Cartesian cubes
Cartesian Genetic Programming
Cartesian Monoids
cartesian-closed
Case study
Catalan numbers
categorial grammar
Categorical Logic
Categorical model
Categorical models
Categorical Quantum Mechanics
Categorical Semantics
Categories of relations
categories with families
Categorification
category
category theory
Causal Dependency
causality preservation
Cautious Reasoning
ccg
CCSL
CDCL
cdcl-cuttingplanes
Cedille
CEGIS
Cellular automata
cellular cohomology
Centrality
certificate checking
certificates
certification
certified code
Certified execution engine
certified software
Certifying Compilation
channel composition
Character-level Language Model
chat bot
chemical computation
Chemical Reaction Networks
Chinese monoids
Choice Logic
choice sequence
Choice sequences
choiceless polynomial time
Chronological Backtracking
Church's type theory
Church-Turing thesis
circuit
Circuit complexity
circuit lower bounds
circuit satisfiability
circular proofs
classical arithmetic
classical B
classical higher-order logic
classical linear logic
classical logic
classical realizability
Classical sequent calculus
Clause Learning
CLF
clocks
closed set
cluster algebra
clustering
CNF
CNF configuration
co-simulation
Coalgebra Modality
Coarse computability
Coarse-grained modeling
CoCoA and MathSAT
codatatypes
code generation
Code Generators
code review
code-generation
coends
Cognitive Modeling
cographs
coherence
coherence theorems
coherent presentations
coinduction
coinduction up-to
Coinductive Invariants
coinductive types
Combination
Combinatorial benchmarks
combinatorial proofs
combinatorial search algorithms
combinatoric
combinatorics
combinators
combinatory logic
common knowledge
Common Language for Geometric Problems
Commonsense Reasoning
commutative monads
Comonads
Comparator
comparator network
comparison systems
CompCert
Competition
compiler
compiler verification
Compilers
complementary approximate reachability
Complementation
complete abstract domains
complete lattices
Complete Segal Spaces
completeness
completion
complex analysis
complexity
Complexity Analysis
complexity classes
complexity dichotomy
Complexity measures
Complexity Proving
complexity results
Complexity theory
composition
compositional analysis of software systems
compositional model checking
compositional reasoning
Compositional verification
compositionality
Computability
computable metric space
computation and deduction
Computation Complexity
Computation Tree Logic
computational complexity
computational effects
Computational Hardness
computational model
Computational modeling
computational monads
Computational Reductions
computational soundness
Computational thinking
computational type theory
computer aided security proofs
Computer Algebra
computer-aided cryptography
concurrency
concurrency and distributed computation
Concurrency Testing
Concurrent datatypes
concurrent dictionaries
Concurrent games
Concurrent objects
Concurrent operation specification
Concurrent Process Calculi
concurrent program algebra
concurrent programs
concurrent separation logic
Concurrent strategies
Condition Synchronization
Conditional Independence
Conditional logic
conditional rewriting
conditional term rewriting
conditional value at risk
confidentiality
conflict-driven clause learning
conflict-driven search
confluence
Confluence Analysis
Confluence and Standardization
confluence competition
Confluence modulo
confluence tool
Confusion
Congruence
Connection-based proof-search
cons-free computation
Conservative approximation
Conservativity
consistency
Consistency Analysis
Consistency Checking
Consistency proofs
constant-time security
Constrained Horn Clauses
Constrained Optimization
constrained rewriting
Constraint Handling Rules
Constraint Handling Rules (CHR)
Constraint Language
Constraint Logic Programming
Constraint Logic Programming on Finite Domains
Constraint Modelling
constraint problem
Constraint programming
constraint satisfaction
Constraint Satisfaction Problem
constraint satisfaction problems
Constraint satisfaction processing
Constraint Solving
Constraint Systems
Constraint-based synthesis
Constraint-based verification
Constraints
constraints solver
constructive
Constructive Decidability
constructive mathematics
Constructive Type Theory
Constructive View of Theories
constructivism
contact logics
context-free
Context-free Grammars
contextual equivalence
contextual fibrancy
contextuality
Continuation Semantics
Continuous computation
Continuous delivery
continuous systems
continuous validation
continuous valuation
Continuous-time Markov chain
contract-based verification
contractibility
Contraction
control
control flow
control improvisation
Control parameters
Control-Flow Refinment
Controlled Natural Language
Controlled Natural Languages
controller synthesis
controller system
conversion algorithm
convex polyhedra
Cooperative Scheduling
Coq
Coq library
Coq proof assistant
Core SAT
Corecursion
correctness
Correctness by extraction
correctness criteria
Correctness Enhancement
Correctness proof
Correctness proofs
Correspondence theory
Cost Analysis
Cost bounded reachability
Cost relations
counter-example
CounterExample Guided Inductive Synthesis
Counterexample-guided Algorithms
Counterexample-Guided Inductive Synthesis
counterexamples
countermodel construction
counting classes
Courcelle's Theorem
Covering Theory
CPS translation
CR-Prolog
CR-Prolog2
Crafted benchmarks
Craig Interpolation
Crime tracing
critical complexity region
critical pair
critical software assurance
Critical Systems
CRN
CRN equivalence
cross-fertilization
cross-section property
crowds
cryptographic CNF instances
cryptographic constant-time
Cryptographic protocol
Cryptographic protocols
cryptographic schemes
Cryptographic software
Cryptography
CSP
CSP Solver
cubical sets
cubical type theory
Curry-Howard
Curry-Howard correspondence
Curry-Howard isomorphism
Cut elimination
cut-elimination
Cut-elimination theorem
Cutting and Packing
Cutting planes
Cyber Security
Cyber-Physical system
cyber-physical systems
Cybercrime
Cycle finding
Cyclic graphs
cyclic induction
cyclic lambda calculus
cyclic proof
Cyclic proofs
cyclic sharing
Cyclic term-graps
Cylindrical Algebraic Decomposition
D
D-optimaldesigns
Daniell-Kolmogorov theorem
data compression
Data Driven modelling
data flow
Data Races
Data words
Data-structures
database theory
Databases
Datalog
datatypes
de Groot duality
Deadlock
Deadlock Analysis
Deadlock Detection
deadlock-freedom
Decentralized planning
decidability
decision
Decision making
Decision Model and Notation (DMN)
Decision Modeling
Decision Modelling
decision procedure
Decision Procedures
decisiveness
declarative algorithms
declarative programming
Declarative Prover
declassification
decoupled approach
decreasing diagrams
deduction
Deductive interactive program verification
Deductive program verification
Deductive programs verification
deductive verification
Dedukti
Deduplication
deep embedding
deep inference
deep learning
Deficiency
definability
Definable
definable while programs
delay differential equations
Delta-completeness
denotation
denotational model
denotational semantics
deontic logis
Dependant Types
dependence maps
Dependency
dependency graph
dependent choice
dependent product types
Dependent Refinement Types
dependent temporal effects
dependent type theory
dependent types
dependently typed programming
derivational complexity
derivationism
Deriving Reliable Programs
Description logic
description logics
descriptive complexity
design automation
Design by contract
Design Space Exploration
destructors
determinacy
Deterministic Automata
Deterministic Parity Automaton
DFA
Diagrammatic Reasoning
dialectica category
Dialectica interpretation
diamond lemma
diffeological spaces
differential dynamic logic
differential equation axiomatization
Differential equations
differential game logic
differential ghosts
Differential Linear Logic
differential programming
Digital libraries
Diller-Nahm variant
Diophantine equations
direct-manipulation interaction
directed complete
Discounted-sum determinization
Discounted-sum inclusion
discrete polymorphism
Discrete-Event
discrete-time linear system
Display calculi
display map category
distance bounding protocols
Distance fraud
Distance-bounding protocols
distribute consensus protocols
distributed autonomous systems
distributed computing
distributed concurrent systems
Distributed Protocols
distributed systems
Distribution based objectives
distributive laws
division
DLVSYSTEM srl
DMN
DNA algorithmic self-assembly
DNF
Dolev-Yao Attacker
domain
domain equation
domain specific languages
domain theory
domain-level strand displacement
domain-specific formal languages
Domain-specific languages
dominance
Double Description method
Double negation
Double-pushout graph transformation
Double-pushout rewriting
downward closures
DPRM Theorem
drat
DRAT proofs
DSL
dual-rail encoding
duality
dualized proof system
Dynamic analysis
Dynamic applications
Dynamic data structures
Dynamic domains
dynamic epistemic logic
Dynamic language
Dynamic Languages
Dynamic Logic
Dynamic nets
Dynamic Partial Order Reduction
Dynamic Programming
Dynamic Verification
Dynamical Systems
E
e-voting
EasyCrypt
Eckmann-Hilton morphism
Economic Reasoning
Economics
effectful bisimilarity
Effective translations
Efficiency
Efficient Attractor
efficient computation
Egraph
Eilenberg-Moore Category
elaboration
Eldarica
Electronic Voting
elementary linear logic
elementary semantics
ellipsoid method
embedded domain specific language
Embedded systems
Empirical evaluation
EMVCo
energy games
energy-efficient computing
engineering mathematics
enriched categories
enriched category theory
entailment check
entailment relation
Entitity Resolution
epistemic logic
Epistemic Logic Program Solvers
Epistemic Logic Programs
Epistemic Negations
epistemic specification
Epistemic Specifications
equality by abstraction over an interval
equational constraints
equational logic
equational rewriting
equational theories
equational theory
Equilibrium Logic
Equivalence
equivalence relations
erasure
Erin
Erin Triples
Erlang
essential unification
essentially algebraic theories
Ethereum
Evaluable Functions
Evaluation
Event Calculus
Event structures
evidential verification
Evolution systems
exceptions
exchange
exchange rule
Executable Harnesses
Executable Specifications
execution time
exhaustive and randomized data generation
Existential Rules
expander graphs
expansion proofs
expected shortfall
Expected Utility
experimental analysis
Experiments
Expert Systems
explainable decision set
Explanation
explanatory analysis
explicit induction reasoning
explicit substitution
Exposed Datapath Architectures
expressiveness
extended resolution
Extension
extensive categories
extensive category
extensive-form games
External calculi
Extraction
F
factorization
fairness
Fairness objectives
false negative rate
false positive rate
Fan Theorem
Fault tolerance
feasibility of functionals
feature tree constraints
fermionic quantum computing
fibrancy of the function type
fibrant replacement
fibred category theory
field theory
Filter
filter models
Finite Automaton
Finite model generator
finite model property
finite model theory
finite multisets
Finite Semantics
finite sum types
finitely partitioned trees
finitization
Firmware
first order theories
First order transduction
first-order combinatorial proofs
First-order list function
first-order logic
first-order logic with inductive definitions
first-order logic with inductive predicates
First-order multiplicative linear logic
First-Order Syntactic Unification
First-order Theory
first-order theory of rewriting
First-order types
Fishbone diagram
Fix-points
fixed parameter complexity
fixed parameter tractable
Fixed Point Arithmetic
fixed point equations
fixed points
fixed-point algorithms for synthesis
fixed-point logic
Fixpoint Algorithms
fixpoint alternation
fixpoint logic
fixpoints
flattener
Floating Point Arithmetic
floating-point
floating-point analysis
floating-point optimization
floating-point round-off errors
flocking
Flow Analysis
flows and nowhere-zero flows
Fly-Automata
FMI
Focused Proof Systems
focused sequent calculus
focused sequent calculus for first-order modal logic
focusing
Focussing
FOIL algorithm
FOL
Forest Algebra
Forest Algebras
Formal Analysis
formal aspects of program analysis
Formal Definition
formal languages and automata theory
Formal Library
Formal Metatheory
Formal Methods
formal methods for security
formal methods in practice
Formal Model
formal proof
formal proofs
formal reasoning
Formal Semantics
formal specification
formal topology
formal verification
formal verification at runtime
Formalisation
formalization
FormalVerification
forward proof-search
four-valued logic
Frama-C
Frames
Free choice sequences
free modules
free monad
Free Variable
Frege systems
Freyd categories
Frobenius algebra
FSM
Full abstraction
Function algebras
Function classes
function package
function summaries
Functional Analysis
functional and relational specifications
functional dependency
functional interpretation
Functional Mock-up Interface
functional programming
functor
functor algebra
functorial spans
fuzz
fuzzer
fuzzy generalization
Fuzzy logic
G
g-leakage
Game semantics
game theory
Games
games and logic
games played on finite graphs
Gandy
Gappa
garbled circuit
generalised operads
generalised species
Generalization of syntactic parse trees
generalized reactivity
Generic Binding Structures
generic proof assistant
Genetic algorithms
Geometric Automated Theorem Provers
geometric realization
Geometry
geometry of interaction
Gillespie algorithm
Girard's translations
global states
gluing
GNATProve
goal-directed evaluation
graded monads
Gradient Boosting on Decision Trees
Gradient descent
Gradual Typing
grammar
Grammar testing
Grammatical Framework
grammatical inference
graph
graph algorithms
Graph Analysis
Graph Drawing
graph encoding
Graph Generation
graph grammars
graph isomorphism
graph minor theorem
graph neural networks
Graph Queries
Graph Recognition
Graph Representation
graph rewriting
graph rewriting systems
graph theory
Graph transformation
Graph Views
Graph Weighted Models
graph-based characterization
Graphical reasoning
Gray categories
Gray category
greatest fixed point
Greedy Heuristics
Groebner bases
Grothendieck fibrations
Grothendieck quasi-topos
ground systems
ground theories
Grounding
Group decision
Groupoid
Gröbner Basis
Guard Condition
Guarded Recursion
Guillotine Constraint
H
Hadamard matrices
halting problem
Hamiltonian cycle
hammers
Handlers
handwriting
Handwritten Digit Recognition
handwritten mathematics
hardness of approximation
Hardware model
hardware verification
hardware-in-the-loop
Hardware/software interfaces
hash functions
Hashing-based Algorithm
Haskell
HCI
head variable
heaps
herbrand theorem
Herbrand's theorem
hereditarily definable sets
hereditary substitution
heuristic search
heuristics
hidden tree Markov model
Hierarchical information
Hierarchical state machines
Hierarchy Theorem
higher categories
higher dimensional categories
Higher dimensional linear rewriting
higher groups
Higher Inductive Type
higher inductive types
Higher order recursion schemes
higher-order
Higher-order abstract syntax (HOAS)
higher-order computability
higher-order logic
higher-order logic programming
higher-order modal logic
higher-order operads
Higher-Order Programs
higher-order reasoning
higher-order recursion schemes
higher-order rewriting
higher-order term rewriting
higher-order unification
Higher-Ranked Polymorphism
Highly Assured Software
Hilbert's tenth problem
Hilbert-Gentzen thesis
HKDF
HMAC
HOL
HOL Light
homogeneous
homogeneous linear diophantine equations
homogeneous types
Homological algebra
Homomorphism
Homotopical algebra
Homotopy
homotopy type theory
Hopf Monad
Horn clause
Horn Clause Transformation
Horn clauses
Horn propositional satisfiability algorithm
howe's method
HW-SW interface
hybrid logic
Hybrid System
hybrid system simulators
hybrid systems
hydraulic oil pump
Hyper sequents
hypercube optimization
Hyperintensional Logic
hyperltl
hyperproperties
Hyperproperty Verification
Hypersequent calculus
hypersequents
I
ic3
IDE
Idempontent
Idempotent quasigroups
identifier
Identity type
IEEE-754
ILP
immunization
imperative
imperative calculi
Imperative languages
imperative programming
imperative programs
Imperfect information
Implementation and benchmarks for parity games
implicate generation
implicative algebras
implicit complexity
Implicit Hitting Set
Importance Splitting
impredicative encodings
impredicativity
inconsistency measures
inconsistency-tolerant reasoning
Inconsistent Requirements Explanation
increasing chains
Incremental
Incremental Analysis
Incremental Maintenance
Incremental SAT
Indexed types
Indistinguishability
induction
induction principle
induction reasoning
induction rules
(PC)
inductive datatypes
inductive definitions
Inductive invariants
Inductive Logic Programming
Inductive predicates
inductive theorem prover
Inductive Theorem Proving
Inductive Types
inductive validity cores
inductive-inductive types
Industrial application
industrial case
industrial impact
inference
inference attacks
infinitary and cyclic systems
Infinitary Proofs
infinitary rewriting
Infinite computation
infinite descent
infinite duration
Infinite modalities
infinite-state systems
Infinite-valued logic
Infinitely nested Boolean structure
Infinity-Categories
Infinity-Presheaves
informal proofs
Information Disclosure Analysis
Information Extraction
information flow
information flow analysis
Information flow control
Injectivity
inner-approximations
innermost conditional narrowing
Insider threat
instantiation
Integer Arithmetic
Integer Transition Systems
integer weights
Integrated Development Environment
integrated verification
integration
integrity
Intension
intensional computation
Intensional Logic
Intensional Sets
Intensional Type Theory
Intentional attack
intentions
interaction graphs
Interaction nets
Interactive system
interactive theorem prover
interactive theorem proving
interactive tool
Interface design
Interlocking
Intermediate Language for Verification
intermediate representations
internal and external calculi
Internal calculi
internal language
internal parametricity
Internet of Things
Interoperability
interpolation
Interpretable Machine Learning
interprocedural analysis
Intersection Type Systems
intersection types
intersections
interval arithmetics
interval propagation
Intrinsic noise
intruder deduction problem
intuitionism
intuitionistic combinatorial proofs
intuitionistic linear logic
Intuitionistic logic
Intuitionistic logic of constant domains
Intuitionistic mathematics
Intuitionistic Modal Logic
intuitionistic propositional logic
Invariant Checking
Invariant Generation
Invariant Synthesis
Invariants
Inverse Reinforcement Learning
IRM-calc
irrelevance
Isabelle
Isabelle Proof Assistant
Isabelle/HOL
Isabelle/HOL Theorem Proving
Isabelle/jEdit
IsaSAT
Isomorphism type
isotopy
Iterated Boolean games
J
JASP
Java
Java byte-code
JDLV
jEdit
JML
Jordan Normal Form
Judgemental Interpretation
Jung-Tix problem
Jupyter
K
k-safety verification
Kachinuki order
Kakutani's fixed point theorem
KeY
key set
kleptography
Knapsack
knot theory
Knowledge Acquisition
Knowledge and belief
Knowledge based Reasoning
knowledge compilation
Knowledge Representation
Knowledge Representation and Reasoning
knowledge-based noninterference
Knuth-Bendix criterion
Koat
Kripke model
L
L-derivative
labelled calculi
labelled calculus
labelled Markov chain
Labelled proof-systems
labelled sequent calculi
Labelled sequents
labelled systems
lambda calculi
lambda calculus
lambda calculus and combinatory logic
lambda prolog
lambda-calculus
lambda-encodings
lambda-free higher-order logic
lambda-prolog
lambda-tree syntax
Lambek calculus
lams
language based security
Language inclusion
large libraries
Large set
large theories
large-scale reasoning
lattice
Lattice Basis Reduction
lattice traversal
lax homomorphism
laziness
lazy
lazy evaluation
lazy grounding
lazy self-composition
Lean proof assistant
learning
Learning from positive examples
learning transductions
Learning Weighted Automata
learning-based testing
Least general generalization
Lemma learning
lens
Leo-III
Leveled sequents
LFSR
Likelihood weighting
Lina
linear algorithm
Linear Arithmetic
Linear categories
Linear Category
linear clauses
linear cliquewidth
Linear Constraints
linear distributivity
linear logic
Linear polygraphs
Linear Programming
Linear Temporal Logic
linear term
linear time hierarchy
Linear Transformations
Linear Tree Constraints
linear-feedback shift register
linear/non-linear logic
Linearity
linearizability
Linearization
Lipschitz maps
Lists
Literate programming
Liveness Analysis
LLVM
Local determinism
Local Theory Extensions
locale theory
Log analysis
logarithmic space computation
logic
logic for PTime
Logic for Teaching
Logic Meta-Programming
Logic of Here and There
Logic on Trees
logic program
logic programming
Logic Programming Applications
Logic Solvers
Logic Tools
Logic-based tools
Logical complexity
logical design
logical formalism
logical framework
Logical Frameworks
Logical models
logical paradoxes
logical predicates
Logical Regulatory Networks
logical relations
logically constrained term rewriting systems
Logics for strategic reasoning
Logistics
LOGSPACE
LOIS
long-distance resolution
loop unrolling
loops
low-level language
Lower Bounds
LPMLN
LPOD
LTI systems
LTLf
lucas interpretation
Lukasiewicz Logics
M
MAC
machine checked proofs
Machine Ethics
Machine Learning
Machine Learning Systems
machine words
magic states
Magic wand
MANET
Maple
MapReduce
MapReduce framework
MARCO
Markov Decision Process
Markov decision processes
Markov processes
Martin-L\"{o}f type theory
Martin-Löf type theory
Mason's Marks
Master Theorem
matching representation
mathematical analysis
Mathematical Induction
Mathematical language
mathematical proof
mathematical proofs
Mathematics
Matita
Matrix Growth
Matrix Interpretation
Matrix semigroups
Maude
maximum realizability
Maximum Satisfiability
MaxSAT
MAXSAT application
MaxSAT resolution
MaxSAT solving
maxSMT
MC-SAT
MCMT
mealy machine
Mean-payoff games
meaningless terms
Measure theory
mechanical reasoning
mechanised theorem proving
mechanized mathematics
mechanized meta-theory
Mechanized proofs
mechanized reasoning
Memoization
Memory
memory consistency models
Memory Errors
memory isolation
memory model
message passing concurrency
Message Passing Interface
meta programming
meta-data library
Meta-Interpretive Learning
meta-programming
Meta-theory
Metamorphic Testing
Metareasoning
metatheory
Metric Semantics
Minimal models
Minimal unsatisfiability
Minimally Adequate Teacher
Minimally strongly connected digraph
Minimisation
Minsky machines
MIPS TLB
Mixed Arithmetic
Mixed Distributive Law
Mixed Integer Linear Programming
ML
MMSNP
Mobile robotics
modal fixpoint logic
modal logic
Modal logics
modal mu
modal mu calculus
Modal type theory
modalities
Model Animation
model checking
Model Checking Games
model construction
Model Counting
Model Expansion
model finding
model generation
Model learning
Model quality
Model Revision
model sampling
Model Theory
Model transformations
model-based engineering
model-based testing
model-checking
Model-checking first-order logic
model-checking problems
Model-level uncertainty
Modeling
Modeling and Specification
Modelling Languages
modelling secure protocols
models
Models of computation
Modular Analysis
modular approach
Modular Arithmetic
Modular System
Modular Tensor Category
modules
Molecular computing
Molecular Filters
Molecular programming
monad
Monadic Second Order Logic
Monads
monitoring
monoid
monoid model
monoidal categories
monoidal category
Monoidal Coalgebra Modality
monotone
Monotone complexity
Monotone proofs
monotonicity
Montague semantics
Montgomery Multiplication
MPI
MSO
MSO on Infinite Words
MSO on omega-Words
MSO transduction
mu-calculus
mu-mutilde-calculus
Multi Factor
Multi Modal logic
Multi-agent models
Multi-agent Systems
Multi-agent workflows
Multi-clock timed automata
Multi-dimensional
Multi-graphs
multi-modelling
multi-objective optimization
Multi-objective synthesis
Multi-party computation
Multi-Pass Dynamic Programming
Multi-player games
Multi-Robot planning
Multi-valued Logic
multicategories
multiplayer games
multiple languages
multiplicative linear logic
Multiplier Verification
multitope
muMALL
N
N player games
nanoCoP
Nanofabricated Devices
narrowing
Nash equilibria
Nash equilibrium
Natural deduction
Natural language
natural language processing
natural language understanding
Natural mathematical language
natural proofs
Natural-style Proofs
Negation as failure
Negation in Logic Programming
Negative translations
neighbourhood semantics
neighbourhood singleton arc consistency
Nelson-Oppen
Nested
nested sequents
nested systems
Network Based Biocomputation
Network Intrusion Detection
Network-free simulation
networks of synchronized automata
neural network
neural networks
Newman's lemma
next state relation
no-go theorem
Noise Reduction
nominal rewriting
nominal terms
nominal unification
nominalizations
non-clausal theorem proving
non-cnf
non-commutative
non-denoting terms
Non-Deterministic Automata
non-deterministic mealy machine
non-idempotency
non-idempotent intersection types
Non-interference
Non-interleaving semantics
Non-lawlike computability
non-linear arithmetic
Non-linear Real Arithmetic
Non-monotonic Reasoning
non-normal modal logic
non-normal modal logics
non-rigid terms
Non-Termination Bugs
Non-termination Proving
non-wellfounded proofs
non-zero sum games
nondeterminism
nonlinear integer arithmetic
NonMonotonic Semantics
nonmonotonic term orders
nonnegativity certificate
nontermination
Normal Form
normal form bisimulation
normal forms
normalisation
normalization
norms
Notation
Notebooks
novel applications domains
Nowhere dense graphs
Numerical optimization
Numerical Program Analysis
Nuprl
Nuprl proof assistant
nuxmv
O
o-minimality
OBDD
Object Constraint Language (OCL)
object-oriented
Object-oriented programs
observational equivalence
OCaml library
Ocra
odd-even network
omega-automata
omega-languages
Omega-regular languages
omega-regular objectives
OMT
Online Decomposition
Online Social Networks
ontologies
Ontology
Ontology Languages
Ontology Reasoning
open games
open set lattice
Open-WBO
OpenFlow
OpenJDK
OpenJML
OpenTheory
Operad
Operating System Verification
operational semantics
Operational Termination
opetope
Optical Networks on Chip
optimal propagation
Optimal Scheduling
Optimal Upper Bound
Optimisation
Optimization
Optimization heuristics
Optimization Modulo Bit-Vectors
optimization techniques
optimizations
OR causality
oracle Turing machines
Order enriched categories
order invariant definability
order theory
order-preserving embeddings
ordered completion
ordered objectives
ordered structures
ordering
ordinal diagram system
Ordinary differential equation
ordinary differential equations
Origin
over-approximation
overt set
Overture
P
Paracoherent Answer Sets
Paraconsistent logic
Parallel computation
parallel improvements
Parallel Processing
Parallel Zielonka's Algorithm
parallelism
parameter optimization
parameter-free axioms
(PC)
parameterised Boolean equation systems
Parameterised verification problem
parameterized AC^0
Parameterized Algorithms
parameterized complexity
Parameterized Model Checking
parameterized systems
parameterized verification
Parametricity
parametrized systems
Parity Game
parity games
parsing
Partial algorithms in Coq
partial correctness
Partial Evaluation
Partial Functions
Partial models
partial order reduction
Partial-order reduction
path orderings
pattern matching
paycheck pronouns
PB constraints
PDL
PDR
PDR-Z3
Peano arithmetic
Perfect masking
perfect samplers
permission inference
permission model
Permissions
Permutation problems
permutations
Persistent places
Petri nets
PGA
phase saving
Phylostatic
Phylotastic
pi calculus
pi-caclulus
Pi-calculus
Picat
Picture Series
Planning
Planning under uncertainty
Plotkin's T
PMCFG
pointer arithmetic
pointfree topology
polarity
Policing function
policy language
Policy Synthesis
polycategories
polygraph
polygraphs
Polyhedra Domain Analysis
Polymers
polymorphism
Polynomial Calculus
Polynomial Factorization
polynomial functor
Polynomial functors
Polynomial hierarchy
polynomial simulation
polynomial upper bounds
polynomial-time tractability
polytyptic programming
population protocols
port graphs
Portfolio
Portfolio Solver
Positive complexity
Post Correspondence Problem
power-law
powerlocale
precision medicine
precondition inference
predecessor function
predicate
Predicate Abstraction
preference
Preference Logic
Preference Modeling
Preferential logics
prefix-constrained term rewriting
premature convergence
preprocessing
presheaf models
presheaf semantics
Presheaves
presupposition
pretty printing
primary key
Prime Numbers
priorities
prism
Privacy
Privacy by design
Privacy-type properties
proactive security
probabilistic
Probabilistic Algorithm
probabilistic bisimilarity
probabilistic bisimilarity distance
Probabilistic Boolean Program
Probabilistic computation
probabilistic CTL
probabilistic finite automata
probabilistic games
Probabilistic graphical models
Probabilistic Inductive Logic Programming
probabilistic lambda-calculus
Probabilistic Logic
Probabilistic logic programming
Probabilistic model checking
Probabilistic planning
probabilistic powerdomains
Probabilistic programs
probabilistic reasoning
Probabilistic rewriting
Probabilistic Satisfiability
Probabilistic State Space Exploration
probabilistic systems
Probabilistic Timed Automata
probabilistic verification
probability
problem database
problem encodings and reformulations
problem fingerprinting
procedural interpretation
process calculi
process calculus
product types
profunctor
Program Analysis
program completion
program correctness
Program Debugging
Program Derivation
Program extraction
Program invariant
Program Projection
program refinement
program semantics
program specialisation
Program Synthesis
program transformation
program transformations
Program translation
Program Verification
Programming by example
programming language semantics
programming languages
programming logic
programming methodology
programming paradigm
Programming-by-Example
progress measure
Projected Model Counting
projective limit
Projective plane
Prolog
Prompt LTL
Proof
proof assistant
proof assistants
proof automation
proof by reflection
proof checker
Proof checking
proof complexity
Proof compression
proof engineering
Proof generation
proof guidance
proof identity
Proof Method Recommendation
Proof Mining
proof nets
proof of literal
proof of univalence
proof schema
Proof search
proof semantics
Proof System
proof systems
proof terms
Proof theory
proof theory of modal logic
Proof translations
proof-as-program
Proof-checker
Proof-Producing Compilation
proof-relevant
Proof-relevant logic
proof-search
proof-theoretic semantics
proof-theoretical linear semantics
proofs
Proofs by reflection
proofs-as-programs
proofs-as-programs-as-morphisms
property directed reachability
property falsification
Property Specification Patterns
property-based testing
Propositional Dynamic Logic
propositional implicational intuitionistic logic
propositional logic
propositional model counting
Propositional Resizing
PROPs
Protocol Verification
protokernel
prototyping
prover
Prover IDE
Prover Trident
proximity relation
Pseudo-Boolean
Pseudo-Boolean Optimisation
Pseudo-Boolean Solving
PSPACE
Public Git Archive
Pushdown systems with transductions
PVS
Python
Q
Q-resolution
QBF
QBF calculi
QDimacs
QRAT
Qualitative Reasoning
qualitative spatial reasoning
qualitattive spatial reasoning
quantale relator
quantification
Quantified Bit-Vectors
quantified boolean formula
Quantified Boolean Formulas
Quantified Circuit
quantified effects
quantified modal logic
quantified modal logics
quantified resolution asymmetric tautology
Quantifier