FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
TALK KEYWORD INDEX

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

#
#SMT(BV)
A
abductive reasoning
abstract interpretation
abstraction-refinement
Ackermann's Lemma
Almost Full relations
Alternating time
applicative first-order logic
Approximation
Armstrong relation
Arrays
automated reasoning
automated theorem proving
Axiom Pinpointing
axiomatization
axioms
B
blocked clauses
Boolean Satisfiability
C
codatatypes
coinduction
Combination
combinatorial proofs
completeness
completion
Complexity
confluence competition
confluence tool
Constraint Satisfaction Problem
Constraint Solving
Constructive Decidability
Craig Interpolation
CSP
D
Datalog
datatypes
decision
decision procedure
Decision Procedures
Deductive program verification
Description logic
description logics
differential game logic
drat
E
equational logic
Existential Rules
explainable decision set
extended resolution
F
feature tree constraints
Finite model generator
first-order logic
First-order Theory
first-order theory of rewriting
Floating Point Arithmetic
Focused Proof Systems
Focussing
H
higher-order logic
higher-order modal logic
higher-order reasoning
HOL
homogeneous
I
Idempotent quasigroups
implicate generation
Implicit Hitting Set
Incremental SAT
Integer Arithmetic
interactive theorem proving
Isabelle
Isabelle/HOL
K
key set
L
lambda-free higher-order logic
Large set
large theories
large-scale reasoning
Leo-III
Linear Arithmetic
Linear Constraints
linear logic
Linear Transformations
logic programming
Logical Frameworks
logically constrained term rewriting systems
Lukasiewicz Logics
M
machine checked proofs
Machine Learning
Maximum Satisfiability
maxSMT
MCMT
Minimisation
Mixed Arithmetic
ML
modal logic
Modal Logics
model construction
Model Counting
models
Multi-valued Logic
N
Nelson-Oppen
next state relation
nonlinear integer arithmetic
nonmonotonic term orders
O
ontologies
P
Parameterized Model Checking
Polynomial hierarchy
Preferential logics
preprocessing
primary key
Probabilistic Algorithm
Probabilistic Logic
Probabilistic Satisfiability
problem database
Program Synthesis
Program Verification
programming logic
proof assistant
proof complexity
Proof compression
proof identity
Proof search
proof systems
Proof theory
Proofs by reflection
propositional logic
prover
Q
QBF
QRAT
Quantified Boolean Formulas
quantified resolution asymmetric tautology
quantifier elimination
Quantifier-free Theory of Arrays
R
reachability
record types
Redundancy-free Proof-Search
Relevance Logic
resolution
restricted chase
rewriting
S
S5
SAT
Satisfiability
Satisfiability Modulo Theories
Satisfiability Modulo Theory
semantic forgetting
separation logic
sequent calculus
SMT
software verification
Static Analysis
static semantics
Structural Operational Semantics
superposition
Symmetry breaking
Syntax-guided Synthesis
synthesis
system description
T
Tableau calculus
Tableaux
term orderings
termination proofs
theorem proving
theories
Time complexity Analysis
tree constraints
tuple-generating dependencies
Type theory
type-logical grammar
U
uniform interpolation
uniform substitution
unions of relations
unit equality
unit propagation
V
vampire
W
weak memory
well-founded relations
witness generation