GLOBAL TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
( | |
(Probabilistic) Integer Programs | |
- | |
- Data Mining | |
- High Utility Itemsets | |
- Propositional Satisfiability | |
0 | |
0-1 integer linear decision problem | |
0-1 laws | |
2 | |
25-years | |
3 | |
3D Space | |
A | |
A.I. in legal practice | |
AB axioms | |
abduction | |
abductive explanations | |
abductive intuitionistic logic | |
abductive logics | |
ABox abduction | |
ABox approximation | |
absolute value maximization | |
Abstract Argumentation | |
Abstract Argumentation Frameworks | |
Abstract machines | |
abstract rewriting | |
Abstract simplicial complexes | |
abstracted action models | |
abstraction | |
abstraction and refinement | |
abstraction refinement | |
Abstraction-Refinement | |
AC-Unification | |
access control | |
Accessibility | |
ACL2(r) | |
Acquisition of conjectures | |
Acting and Sensing | |
Action and change | |
Action languages | |
action model learning | |
Actions | |
active action model learning | |
active learning | |
activity recognition systems | |
Actual Causality | |
acyclicity notions | |
ad-hoc overloading | |
Adaptive Search Heuristic | |
additive combinatorics | |
Administrative Discretion | |
adversarial contexts | |
adversarial robustness | |
Adversarial Training | |
adversary argument | |
Agda | |
Agent autonomy | |
agent interrogation | |
agent programs | |
aggregates | |
AI ethics | |
AI Safety | |
Airline scheduling | |
ALC | |
algebra interpretations | |
Algebraic Circuits | |
Algebraic Data Types | |
Algebraic Geometry | |
algebraic graph rewriting | |
algebraic hierarchy | |
Algebraic Measures | |
Algebraic Model Counting | |
algebraic number theory | |
algebraic structures | |
Algorithm Portfolio | |
Algorithm Selection | |
Algorithms | |
almost stable matching | |
almost-sat | |
alpha-equivalence | |
alphabetic equivalence | |
amalgamation property | |
Ambiguity | |
amortised cost analysis | |
analytic tableaux | |
Angluin algorithm | |
answer set | |
Answer Set Counting | |
Answer Set Navigation | |
Answer Set Programming | |
Answer Set Programming (ASP) | |
Answer set programming in dynamic domains | |
Answer Sets | |
answer-set programming | |
Anti-Unification | |
Any-space Algorithms | |
Anytime MaxSAT | |
API | |
Application | |
Applications | |
Applied topology | |
Approval Voting | |
approximate counting | |
Approximate Reasoning | |
Approximation Fixpoint Theory | |
Archive of Formal Proofs | |
argument mining | |
Argumentation | (ABR 2022) |
Argumentation and law | |
Argumentation Framework | |
arithmetic | |
Arithmetic Circuits | |
arithmetic constraints | |
Arrays | |
Artificial Intelligence | |
Artin gluing | |
ASP | |
ASPIC+ | |
Assemblies | |
Associativity | |
Assume-Guarantee Synthesis | |
Assumption-based argumentation | |
assumption-based reasoning | |
assumptions | |
Asynchronicity | |
at least three keywords must be specified | |
attacker advantage | |
auditable solving | |
authenticated encryption | |
authentication | |
automata | |
automata theory | |
automated algorithm configuration | |
automated algorithm design | |
Automated Deduction | |
Automated ethics | |
automated grading | |
automated instance generation | |
Automated planning | |
automated planning and scheduling | |
Automated proofs | |
Automated reasoning | |
Automated Testing | |
automated theorem proving | |
Automatic Complexity Analysis | |
Automatic program verification | |
automatic reformulation | |
automatic structures | |
automatic test-case reduction | |
automatic theorem proving | |
automatic verification | |
Automating Commonsense Reasoning | |
automation | |
automatizability of proof systems | |
Autonomous systems | |
auxiliary | |
availability | |
Average-case complexity | |
awards | |
axiom of choice | |
Axiomatic Systems | |
B | |
back-and-forth method | |
back-translation | |
backdoor attack | |
backdoor depth | |
backdoor sets | |
Backdoors | |
Backreferences | |
Backtracking | |
Banach-Tarski | |
Bar Recursion | |
Basic education | |
battle of Hercules and Hydra | |
Bayesian Machine Learning | |
Bayesian network classifiers | |
Bayesian Network Structure Learning | |
BDD | |
Behavioural equivalence | |
Belief | |
Belief Base | |
belief base change | |
Belief bases | |
belief change | (BCORE-22) |
Belief Contraction | |
Belief Fusion | |
Belief Merging | |
Belief Revision | (BCORE-22) |
belief update | |
benchmarking | |
benchmarks | |
Bernays–Schönfinkel Fragment | |
Beth Definability Property | |
betterness relation | |
Beyond NP | |
bi-objective optimization | |
Biased graphs | |
Bicategories | |
bidirected | |
big data | |
binary codes | |
Binary Constraint Tree | |
Biological Systems | |
bipolar argumentation | |
bisimilarity | |
bisimulation | |
bit pigeonhole principle | |
Bit-precise Reasoning | |
Bit-vectors | |
blackboard | |
Blake Canonical Form | |
Block cipher modes | |
blockchain | |
Boolean algebra | |
Boolean algebras | |
boolean classifiers | |
boolean games | |
Boolean Network Synthesis | |
Bounded arithmetic | |
bounded cliquewidth | |
bounded expansion | |
Bounded model checking | |
bounded value iteration | |
bounded-depth Frege | |
boundedness problem | |
bounds | |
BPMN | |
branch-and-bound | |
branch-and-cut | |
branching bisimulation | |
browser | |
Bryant | |
bug minimizer | |
Building Design | |
Building Information Modelling | |
Bunched Logic | |
bundled fragment | |
business meeting | |
Büchi automata | |
C | |
Cache | |
cache coherence | |
Calculus of Names | |
Call by value | |
Call-by-name | |
call-by-push-value | |
Call-by-value | |
canonical structures | |
canonicity | |
canonization | |
capabilities | |
capability machines | |
Cardinal Directional Calculus | |
Cardinality Constraints | |
case study | |
Catamorphisms | |
Categorical models | |
categorical semantics | |
categories with families | |
Category | |
category theory | |
Cauchy integral formula | |
Cauchy-Goursat theorem | |
causal graph | |
causal graphs | |
causal inference | |
causality | |
CDCL | |
CDCL based Sampling | |
CDSAT | |
certificate checking | |
Certificates | |
certification | |
Certified Algorithms | |
certifying algorithms | |
characterization | |
Chase termination | |
Checked C | |
cheminformatics | |
chi-boundedness | |
Choice logics | |
choice operator | |
Choice sequences | |
Choiceless Polynomial Time | |
chordal graphs | |
choreography | |
Chu construction | |
Church encoding | |
Church's thesis | |
Chvátal-Gomory cuts | |
circuit complexity | |
circuit satisfiability | |
Circular proofs | |
Circumscription | |
class field theory | |
Class hierarchy | |
Classical Logic | |
Classical Model of Science (CMS) | |
classical planning | |
classical realizability | |
Classification | |
classification instance | |
clausal tableaux | |
clause learning from simple models | |
clause redundancy | |
clause sharing | |
clique | |
clique-width | |
Closed Form | |
closure redundancy | |
Cloud Security | |
Clustering | |
CNF | |
CNF encoding | |
CNF translation | |
Co-stable Model Semantics | |
coalgebra | |
Cognitive Reasoning | |
Cognitive robotics | |
coherence | |
Coinduction | |
coinductive type | |
collective attacks | |
Collective Entity Resolution | |
collusion-free protocols | |
collusion-preserving protocols | |
Color refinement algorithm | |
Coloring | |
Combination Problem | |
combinatorial optimisation | |
Combinatorial optimization | |
combinatorial proofs | |
combinatorics | |
combinatorics on words | |
combinators | |
combinatory logic | |
combining decision procedures | |
Commonsense reasoning | |
Commutation | |
Commutativity | |
comonads | |
compatibility | |
Competition | |
competitions | |
compilation | |
compilation scheme | |
Compiler | |
compiler verification | |
complementation | |
complete proof system | |
Complete Search Algorithms | |
Completeness | |
Completeness guarantees | |
Completeness/Soundness | |
Completion of an Ordering | |
complex analysis | |
Complexit and decidability | |
Complexity | |
complexity analysis | |
component based modeling | |
composite event recognition | |
Compositional Synthesis | |
Compositional Verification | |
Compound conditionals | |
comprehensibility | |
Computability | |
computability theory | |
Computable analysis | |
computable isomorphisms | |
computational and-or graphs | |
computational aspects of argumentation | |
Computational Complexity | |
computational effect | |
computational interpretation | |
Computational Law | |
computational models of argument | |
Computational Security | |
computer-aided cryptography | |
computer-assisted proof | |
computer-checked proofs | |
Computing Education | |
computing explanations | |
computing termination probability | |
concentration inequalities | |
Concept Referring Expressions | |
conceptual design | |
Concrete sheaves | |
concurrency | |
concurrency theory | |
Concurrent Programs | |
Concurrent Separation Logic | |
condensed detachment | |
Conditional belief base | |
Conditional effects | |
conditional logic | |
Conditional logics | |
Conditional objects | |
conditional obligation | |
Conditional planning | |
Conditional previsions | |
conditional reasoning | |
Conditional Term Rewriting Systems | |
Conditionals | |
Condorcet Jury Theorem | |
Conflict Analysis | |
conflict management | |
Conflict Resolution | |
Conflict-driven constraint learning | |
conflicts | |
confluence | |
Conformance Checking | |
congruence extension property | |
Conjunctive Queries | |
Conjunctive query entailment | |
connectedness | |
connection structure calculus | |
Connection tableaux | |
consensus | |
consequence relations | |
conservative extensions | |
consistency | |
Consistency Checking | |
constant depth Frege | |
constrained default logic | |
Constrained Horn Clauses | |
Constrained Single-Row Facility Layout Problem | |
constrained term rewriting | |
constraint | |
Constraint Acquisition | |
Constraint and logic programming | |
Constraint Horn clauses | |
Constraint learning | |
Constraint Modelling | |
Constraint Optimisation Problems | |
Constraint Optimization Problems | |
constraint programming | |
Constraint propagation | |
constraint satisfaction | |
Constraint Satisfaction Problem | |
Constraint satisfaction problems | |
Constraint simplification | |
constraint solving | |
Constraint tableaux | |
Constraints | |
Constraints translation | |
constructive algebra | |
constructive matemathics | |
constructive mathematics | |
constructive type theory | |
Contamination Constraints | |
Context-free languages | |
continuous processes | |
continuous reachability | |
Contracts | |
contrastive explanations | |
control synthesis | |
Control-Flow Refinement | |
Controlled Natural Language | |
controlled natural languages | |
Controller Synthesis | |
convex polyhedra | |
Cooperative agents | |
copy-discard categories | |
Coq | |
Coq community | |
Coq library | |
coq plugin | |
Coq-Elpi | |
core extraction | |
corecursive function | |
correct-by-construction | |
correction sets | |
correspondence | |
cost function network | |
cost models | |
countably basic monad | |
counter automata | |
counter systems | |
Counterexamples | |
counterfactual explanations | |
Counterfactual Reasoning | |
Counterfactuals | |
countermodel construction | |
Counting Complexity | |
Counting Proof Systems | |
Counting queries | |
covert channels | |
CPAchecker | |
Craig interpolants | |
Craig interpolation | |
Critical Pair | |
Critical Pairs | |
cryptography | |
CS education | |
CS-TRSs | |
CTL* | |
CTRSs | |
cube-and-conquer | |
cubical sets | |
Cubical Type Theory | |
Curry-Howard | |
Curry-Howard correspondence | |
Cut Elimination | |
cut-elimination | |
cutting planes | |
cyclic dependencies | |
cyclic proof | |
Cyclic proofs | |
cyclicity | |
cylindrical algebraic coverings | |
D | |
d-privacy | |
Darwiche-Pearl | |
Data analysis | |
data federation | |
data graphs | |
data logics | |
Data mining | |
Data Quality | |
data representation | |
Data Structures | |
Data Transfer | |
data words | |
data-driven algorithm design | |
Data-driven invariant learning | |
Data-driven methods | |
databases | |
dataflow programming | |
Datalog | |
Datalog rules | |
Datalog± | |
DCOP | |
DDoS attacks | |
debugging | |
decidability | |
decidable fragments | |
Decidable Subclasses | |
deciding almost sure termination | |
decision diagrams | |
decision procedure | |
decision tree | |
Decision trees | |
Declarative Framework | |
declarative modeling language | |
declarative problem solving | |
Declarative Process Mining | |
declarative programming | |
Decomposition | |
decreasing diagrams | |
Deducibility | |
Deductive Database Method | |
Deductive database method for geometry | |
deductive interpolation property | |
Deductive System | |
Dedukti | |
Deep Embedding | |
deep generative models | |
Deep inference | |
deep learning | |
Deep Learning Compiler | |
deep neural networks | |
Deep Probabilistic Modelling | |
Deep Probabilistic Programming Languages | |
Deep reinforcement learning | |
Default logic | |
Defeasible and preferential logics | |
Defeasible Knowledge | |
defeasible reasoning | |
Defeat Notions | |
Defeaters | |
Defense Notions | |
definability | |
definite descriptions | |
definition by cases | |
Definition Variables | (QBF2022) |
definitions | |
degrees of explainability | |
Delegate Reasoner | |
Denotational semantics | |
density | |
deontic cube | |
Deontic Logic | |
dependency pairs | |
dependency trees | |
dependent right adjoints | |
dependent type theory | |
dependent types | |
Description Logic | |
Description Logic EL | |
Description Logics | |
Description logics with fixpoints | |
Description logics with transitive role closure | |
Descriptive Complexity | |
Design Automation | |
deterministic hierarchies | |
Determinization | |
development closed critical pairs | |
Diagonalizable matrices | |
Diagrammatic language | |
Dial A Ride | |
dialectical explanations | |
Dialogue For Explanation | |
dichotomy theorem | |
Difference logic | |
Differential Categories | |
differential dynamic logic | |
Differential linear logic | |
differential privacy | |
Digital Forensics | |
Digital ICs | |
digraphs | |
Dijkstra commands | |
diophantine equations | |
diophantine sets | |
directed acyclic graphs | |
directed type theory | |
Discrete Morse theory | |
Discrete Optimization | |
disjointness | |
disjunctive programs | |
Disjunctive Rules | |
Display calculus | |
distance bounding | |
distant attacker | |
Distributed algorithms | |
distributed automata | |
Distributed Synthesis | |
Distributed Systems | |
Distribution semantics | |
distributive laws | |
divergence theorem | |
Diversity of Solutions | |
Divide-and-Conquer | |
division | |
DL | |
DL Workshop | |
DL-Lite | |
DL-Lite-Horn | |
DLV | |
document stores | |
domain-specific language | |
domain-specific languages | |
Domains | |
Dominance Breaking | |
dot-depth hierarchy | |
double push out approach | |
double pushout approach | |
DP-3T | |
DPRM theorem | |
DQBF | |
DQBF Solver | |
DRAT proofs | |
dyadic deontic logic | |
Dynamic consistency checking | |
Dynamic Deontic Logic | |
Dynamic epistemic logic | |
Dynamic Programming | |
dynamic release | |
dynamic symmetry breaking | |
Dynamics in Argumentation | |
E | |
E-unification | |
E-voting | |
EasyCrypt | |
Eckmann-Hilton | |
education | |
Effective algorithms | |
Efficient reasoning | |
Eisbach method | |
EKE | |
EL | |
EL ontologies | |
Electric power network | |
Electron | |
electronic voting | |
element-free probabilities | |
elementary computation | |
elementary functions | |
Elpi | |
Emaj-SAT | |
embarrassingly parallel search | |
Embedding Space | |
Emerson-Lei acceptance | |
Emerson-Lei automata | |
emptiness | |
Emscripten | |
emulation | |
encoding | |
Enforcement | |
enriched monad | |
entailment | |
Entailment problem | |
Enthymemes | |
Entropy Estimation | |
enumeration | |
Epistemic Deontic Logic | |
Epistemic logic | |
Epistemic Logics | |
Epistemic State | |
Epistemic States | |
epistemic uncertainty | |
equational logic | |
equational theories | |
equational unification | |
equivalence | |
Erlang | |
Ethereum | |
Ethereum 2.0 | |
Ethical Reasoning | |
Euclidean Geometry | |
EuroProofNet | |
evaluation | |
evaluation order | |
Event Calculus | |
Events | |
Eventual non-negativity | |
everybody | |
Ewens distribution | |
exact computation | |
Exact Learning | |
existential rules | |
expectation transformer | |
Expected runtime | |
Expected Runtimes | |
Expected Sizes | |
experimental evaluation | |
experiments | |
Expert Systems | |
expertise | |
Explainability | |
Explainable AI | |
Explainable AI Planning | |
Explainable Artificial Intelligence | |
Explainable Logic | |
Explainable planning | |
explanation | |
Explanation Sequence | |
explanations | |
explicit definability | |
explicit substitutions | |
Exponential local-global principle | |
Exponential maps | |
Exponentials | |
expressive DLs | |
Expressive power | |
expressiveness | |
Extensional Type Theory | |
F | |
factor interpretation | |
fair exchange | |
fairness | |
Fairness Verification | |
fallacious argumentation | |
Fallible sensors | |
Farkas' Lemma | |
fault isolation | |
feasible fragments | |
feedback | |
fibrations | |
Filtering algorithm | |
fine-grained locking | |
finite abstraction | |
finite axiomatizability | |
finite constraint languages | |
Finite entailment | |
finite fields | |
finite model theory | |
finite models | |
Finite-state abstractions | |
finitely basic monad | |
finitely subdirectly irreducible | |
finiteness | |
first-order ATP | |
first-order logic | |
first-order logic with equality | |
first-order modal logic | |
first-order reasoning | |
First-order rewritability | |
First-order theorem proving | |
first-order theory of rewriting | |
first-order theory of the reals | |
fixed point | |
fixed point theory | |
fixed points | |
Fixed-domain semantics | |
Fixed-Parameter Tractability | |
Fixed-Point Logic | |
fixpoint | |
fixpoint logic | |
Fixpoint Semantics | |
FL0 | |
FL0 and FLbot | |
FLbot | |
Floating-Points | |
fluted fragment | |
FOL | |
Forecasting | |
Forgetting | |
formal languages | |
Formal mathematics | |
Formal Methods | |
formal methods and verification | |
formal modeling | |
formal proof | |
Formal Proof Techniques | |
formal proofs | |
formal semantics | |
formal verification | |
formalization | |
formalization of category theory | |
formalization of mathematics | |
Formula Simplification | |
free algebras | |
free-choice nets | |
Frequency Moments | |
Full-angle Method | |
full-system guarantees | |
Function algebras | |
Function Symbols | |
functional analysis | |
functional big-step semantics | |
Functional correctness verification | |
Functional Data Structures | |
Functional logic programming | |
Functional Machine Calculus | |
functional programming | |
Functor of points | |
futures | |
Fuzz Testing | |
Fuzzing | |
Fuzzy Description Logics | |
fuzzy logic | |
Fuzzy proximity relations | |
Fuzzy Subsumption | |
G | |
Gaifman Normal Form | |
Gale-Shapley Algorithm | |
game comonads | |
games | |
games on graphs | |
Garbage Collection | |
Gauge integral | |
GDPR enforcement | |
general game playing | |
generalisation | |
generalised soundness | |
Generalization | |
generalization guarantees | |
Generalized applications | |
generalized policies | |
generalized soundness | |
generalized stable model | |
Generating Benchmarks | |
Generating functions | |
generative power | |
generic effects | |
Genetic Programming | |
Geometry automated theorem provers | |
Geometry Problem Solving | |
Gini index | |
global constraints | |
gluing | |
goal-directed | |
Goal-Directed Answer Set Programming | |
Goal-Directed evaluation | |
GPU | |
graded modalities | |
Graded monads | |
Gradual Argumentation | |
gradual semantics | |
grammar-based tree compression | |
graph coloring | |
graph grammar | |
graph isomorphism | |
graph neural networks | |
graph node property prediction | |
graph partitioning | |
graph rewriting | |
graph theory | |
graph transformations | |
Graph-minors | |
graphical calculus | |
graphical feedback | |
graphical models | |
graphs | |
greedy decomposition | |
Green's theorem | |
Gringo | |
ground joinability | |
ground term similarity relations | |
Grounded Theory | |
group cohomology | |
Group Reliability | |
Groupoids | |
guarded fragment | |
guarded recursion | |
Gödel logic | |
Gödel logics | |
H | |
hardware | |
hardware tokens | |
Haskell | |
Heterogeneous knowledge bases | |
heuristic algorithms | |
heuristics | |
Hierarchical Models | |
High School Students | |
higher categories | |
higher category theory | |
Higher Inductive Types | |
higher observational type theory | |
Higher order computation | |
higher-order | |
higher-order deduction | |
Higher-order logic | |
higher-order modal logic | |
Higher-Order Pattern Rewrite System | |
Higher-order rewriting | |
higher-order term rewriting | |
higher-order unification | |
Hilbert space | |
Hilbert-style proof systems | |
hitting formulas | |
hoare logic | |
HOL Light | |
HOL4 | |
homological algebra | |
homomorphic encryption | |
homotopy | |
homotopy type theory | |
Horn formula | |
Horn theories | |
Horn-DL | |
Horn-fragments | |
HTN Planning | |
human computer interaction | |
human reasoning | |
Human-Aware AI | |
Human-Computer Interaction | |
Human-robot collaboration | |
Hybrid Knowledge Bases | |
Hybrid Logic | |
Hybrid MKNF Knowledge Bases | |
Hybrid planning | |
hybrid reasoning | |
Hybrid Systems | |
Hyper-parameter optimisation | |
Hyper-parameters tuning | |
hyperdoctrine | |
hyperintensionality | |
Hyperliveness | |
HyperLTL | |
Hyperproperties | |
Hypersequent calculi | |
Hypersequents | |
I | |
iALC | |
identity management | |
Imperative language | |
imperative program | |
implementation | |
implementations | |
implementing sequent calculi in Prolog | |
Implicit Complexity | |
Implicit Computational Complexity | |
implicit deletion | |
implicit hitting set approach | |
Implicit hitting set duality | |
Important separators | |
Impredicative universe | |
Incidence Graph | |
incompleteness | |
inconsistency-tolerant semantics | |
incremental CDCL | |
incremental MaxSAT | |
incremental SAT | |
Independent Hashing | |
Indistinguishability | |
induction | |
Induction and coinduction | |
Inductive inference | |
inductive inference operator | |
Inductive Logic Programming | |
Inductive reasoning | |
inductive theorem proving | |
infeasibility | |
inference | |
inference schemas | |
infinite duration | |
infinite proofs | |
infinite stable models | |
infinite-domain constraint satisfaction problem | |
infinite-state systems | |
information extraction | |
information flow | |
information flow control | |
Information leakage | |
Information-flow security | |
inherently weak automata | |
Inner-approximation | |
Insertion Variables | |
instantiation | |
Integer Difference Logic | |
Integer encoding | |
integer programming | |
Integer Programs | |
integer transition systems | |
intelligent tutoring | |
intelligent tutoring system | |
intensional concepts | |
Interactive Explanations | |
interactive textbook | |
Interactive Theorem Proving | |
Interactive Web System | |
Interference-based proofs | |
Intermediate conditions and effects | |
Intermediate Logics | |
Internet of Things | |
Interpolation | |
Interpretability | |
interpretable models | |
Interpretable prediction | |
interpretation | |
interpretations | |
Intersection Types | |
introduction | |
Intuitionism | |
intuitionistic linear logic | |
intuitionistic logic | |
Invariance | |
Invariant synthesis | |
invertibility | |
Invited Talk | |
iPRA | |
Iris | |
ISA specification | |
Isabelle | |
Isabelle Proof Assistant | |
Isabelle Sledgehammer | |
Isabelle/HOL | |
Isabelle/jEdit | |
Isabelle/VSCode | |
isolation problem | |
isomorph-free exhaustive generation | |
isomorphism | |
Iterated Belief Change | |
Iterated Belief Revision | |
J | |
Java - C - Haskell - Prolog | |
JavaScript | |
Job-shop Scheduling Problem | |
JSON documents | |
Judgment Aggregation | |
Justifiable Exceptions | |
justification | |
Justification Logic | |
justification theory | |
justifications | |
K | |
k-SAT | |
KALM | |
Kan-Quillen model structure | |
Kant | |
Kemeny Rank Aggregation | |
Kernel Contraction | |
kernelization | |
key agreement | |
key exchange | |
key hierarchy | |
Keyword1 | |
Keyword2 | |
Keyword3 | |
Kleene Algebra | |
Kleene star | |
knapsack | |
knowability | |
Knowledge | |
knowledge authoring | |
Knowledge base | |
Knowledge Based Data Management | |
knowledge compilation | |
Knowledge Diversity | |
knowledge extraction | |
Knowledge graph | |
Knowledge Graphs | |
Knowledge integration | |
knowledge representation | |
Knowledge representation and reasoning | |
Kolmogorov complexity | |
Koopman operator | |
kr | |
KR and Machine Learning | |
Kripke semantics | |
L | |
Labelled Tableaux | |
Labelled Transition Systems | |
Lafont category | |
Lambda calculus | |
lambda-abstraction | |
lambda-calculus | |
lambda-mu-calculus | |
Lambek calculus | |
language | |
Language inclusion | |
Language of a knowledge base | |
language-based mechanisms | |
language-based security | |
large neighborhood search | |
Large Neighbourhood Search | |
Large Prime Fields | |
large-neighbourhood search | |
LARS | |
lattice theory | |
Lattice-based many-valued logics | |
Law of Excluded Middle | |
Lazy clause generation | |
lazy encoding | |
Lazy paramodulation | |
Le\'sniewski | |
Lean | |
Lean prover | |
Learning | |
learning capabilities | |
learning decision trees | |
learning from examples | |
Learning from Time-series Data | |
learning policies | |
Least General Generalizations | |
Legal Reasoning | |
Legal Rule Modelling | |
Legal Technology | |
Legendre PRF | |
lemma generation | |
Letrec languages | |
lexicographic inference | |
Leximax | |
Library | |
library design | |
Library of encodings | |
lifted strips | |
Linear Algebra | |
Linear Approximation | |
Linear Arithmetic | |
Linear Bounding | |
linear constraints | |
Linear dynamical systems | |
linear equations | |
Linear Integer Arithmetic | |
linear logic | |
linear loops | |
Linear programming relaxation | |
linear real | |
Linear recurrence sequences | |
linear temporal logic | |
Linear Temporal Logic on finite traces (LTLf) | |
Linear Time Logic | |
Linear-time/branching-time spectrum | |
Linearisation | |
linearize arithmetic | |
Linicrypt | |
Linkability | |
linter | |
list | |
literate programming | |
Liveness | |
LLVM | |
lob induction | |
local consistency | |
local deduction theorem | |
Local Search | |
local verification | |
local-time semantics | |
Locality | |
locally presentable category | |
Log Generation | |
Logarithmic Space | |
Logic | |
logic for PTime | |
logic languages | |
Logic Locking | |
logic methods | |
Logic of Here-and-There | |
Logic of Paradox | |
logic program splitting | |
logic programming | |
logic programming and automated reasoning | |
Logic Programming and Machine Learning | |
logic-based ontologies | |
Logical Atomicity | |
Logical Constraints | |
Logical Entailments | |
logical framework | |
Logical Frameworks | |
logical relations | |
Logics for Multi-Agent Systems | |
Logics of uncertainty | |
Lookaheads | |
loop acceleration | |
Loop Invariant Generation | |
Lossy channel systems | |
Low-complexity Description Logics | |
lower bound | |
lower bounds | |
lower runtime bounds | |
Lower-regular | |
LP^MLN | |
LREC | |
LTI | |
LTL | |
LTLf synthesis | |
M | |
machine learning | |
machine learning classifiers | |
Machine Learning Compiler | |
machine learning theory | |
Machine Reasoning | |
magic wand | |
maintainability | |
Many-Sorted Logic | |
MAP inference | |
Marine Exploration | |
Maritime Traffic Control | |
Markdown | |
Markov categories | |
Markov decision processes | |
Markov equivalence | |
Martingales | |
Match-bounds | |
Matching | |
matching modulo AC | |
Mathematical Components | |
Mathematical Formalisation | |
Mathematical fuzzy logic | |
Mathematical Knowledge Exploration | |
Mathematical Learning Environment | |
mathematical proofs | |
Mathematics | |
Mathematics Education | |
mathlib | |
Matrix Algebra | |
matroid | |
Max#SAT | |
max-sat | |
Max-SAT Resolution | |
maximum clique | |
maximum satisfiability | |
MaxSAT | |
Mazurkiewicz Traces | |
MDD | |
Mean payoff | |
measure theory | |
Mechanism Design | |
mechanization | |
mechanized proofs | |
membership | |
membership inference | |
Memory allocation | |
Memory automata | |
memory sharing | |
message passing | |
Meta Logic Solving | |
meta-programming | |
Metaheuristics | |
metric differential privacy | |
metric spaces | |
metric temporal queries | |
metrics | |
Minimal tableau | |
Minimal typings | |
minimal unsastisfiable set | |
Minimalist Type Theory | |
minimality criterion | |
Minimally Unsatisfiable Subsets | |
Minimum description length | |
minimum explanations | |
minimum hitting sets | |
Mixed Integer Progamming | |
mixed integer programming | |
Mixed-Integer Programming | |
Mizar | |
MKNF | |
modal logic | |
Modal logics | |
modal mu-calculus | |
modal operators | |
modal type theory | |
modalities | |
model building | |
model checking | |
Model Checking Problem | |
Model Counter | |
Model Counting | |
model learning | |
Model reconciliation | |
Model Synthesis | |
model theory | |
model-based reasoning | |
Model-Checking | |
Modeling | |
Modelling | |
models of computation | |
modular circuits | |
Modular Reasoning | |
Modular termination | |
modularity | |
module system | |
monadic decomposability | |
monadic dependence | |
monadic embedding | |
monadic second-order logic | |
monadic stability | |
monads | |
monoidal category | |
monoidal closed categories | |
monoidal stream | |
monotone circuits | |
monte carlo | |
Monte Carlo techniques | |
Most specific concept | |
Motion planning | |
MSC Languages | |
mu-calculus | |
Multi--One Peak | |
Multi-Agent Debate | |
multi-agent epistemic logic | |
Multi-Agent Path Coordination | |
Multi-Agent Systems | |
Multi-context systems | |
Multi-homomorphism | |
multi-modal verification | |
Multi-Objective Optimisation | |
Multi-objective optimization | |
multi-paradigm | |
Multi-shot solving | |
multi-valued decision diagrams | |
Multilayer Perceptrons | |
multinomial theorem | |
multiparty communication complexity | |
multiparty computation | |
Multiplicative-additive fragment | |
multiset | |
multiset rewriting | |
multistep reduction | |
Multiwinner Voting | |
muMALL | |
music composition | |
mutation | |
N | |
Narrowing strategies | |
Nash Equilibria | |
Natural Deduction | |
natural language generation | |
natural language processing | |
natural semantics | |
Negation as Failure | |
negative knowledge | |
Negative Statements | |
negative translation | |
negotiations | |
nested regular path queries | |
Nested sequent | |
Nested sequent calculus | |
Network security | |
Networks | |
networks/graphs | |
neural network | |
Neural Network Models | |
Neural Network Verification | |
neural networks | |
Neural networks verification | |
neural symbolic learning | |
Neural-symbolic integration | |
Neuro-Symbolic | |
neuro-symbolic AI | |
neuro-symbolic computing | |
Neuronal networks | |
NFA | |
NLP | |
NMatrices | |
nominal algorithms | |
nominal logic | |
Nominal Techniques | |
Non-classical Logic | |
non-classical logics | |
Non-classical Semantics | |
non-deterministic semantics | |
non-interactive key exchange | |
Non-linear constraints | |
non-linear reasoning | |
non-monotonic logic | |
Non-monotonic logical reasoning | |
non-monotonic reasoning | |
Non-monotonic reasoning in DLs | |
Non-normal modal logics | |
Non-optimality of proof systems | |
Non-prioritised revision | |
non-redundant clause learning | |
non-termination | |
Nondeterminism | |
Nondisjoint theories | |
noninterference | |
nonlinear real arithmetic | |
nonmonotonic reasoning | |
Normal Logic Programs | |
Normalisation | |
normalization | |
normalization by evaluation | |
Normative Systems | |
notebook | |
nowhere dense | |
Nullstellensatz | |
Number Fields | |
O | |
OBDA | (DL 2022) |
OBDD | |
OBDD-based proof systems | |
Object-Centric Event Logs | |
observational equivalence | |
off-line guessing | |
OMQA | |
online | |
Online Grounding of Planning Domains | |
online LTL monitoring | |
Online Planning | |
online teaching | |
ontological argument | |
ontologies | |
ontology | |
ontology alignment | |
Ontology Based Data Access | |
ontology extension | |
Ontology repair | |
Ontology-based data access | |
ontology-mediated query | |
Ontology-mediated query answering | |
ontology-mediated querying | |
Open Challenges | |
open problems | |
open relation extraction | |
opening | |
operational and denotational semantics | |
operational semantics | |
operator | |
Optimal ABox Repair | |
optimal proof systems | |
optimisation | |
optimization | |
Optimization Algorithms | |
orbit-finite sets | |
Order-Sorted Logic | |
Ordered Disjunction | |
Ordered Local Confluence | |
Ordered Multivalued Decision Diagram | |
Ordinal Conditional Functions | |
organization | |
oudenadic embedding | |
OWL | |
P | |
P4 language | |
PAC learning | |
PAC semantic | |
packed classes | |
packing coloring | |
PAKE | |
Panel | |
Paraconsistency | |
parallel algorithms | |
parallel branch-and-bound | |
parallel computation | |
Parallel Machine Scheduling | |
Parallel Sorting Algorithms | |
parallel-innermost rewriting | |
Parameter learning | |
parameterised Boolean equation systems | |
parameterized complexity | |
Parametric continuous-time Markov chains | |
parametric solution | |
paramodulation | |
pareto front enumeration | |
Parity automata | |
Parmeterized Algorithms | |
parser | |
partial Horn theory | |
partial programs | |
Partial Stable Models | |
partial-order methods | |
partition | |
Passive Learning | |
path induction | |
path orders | |
path-aware Internet architectures | |
pathwidth | |
Patient Transportation | |
PBPO+ | |
PDF.js | |
Peano arithmetic | |
pebble-relation | |
Perception & Reasoning | |
perfect matching | |
performance | |
performance prediction | |
Permitted Announcements | |
permutation equivalence | |
Perspectives | |
petri nets | |
phase distinction | |
Physical observable | |
pi-forall | |
Pigeonhole Principle | |
Plan execution monitoring | |
planning | |
Planning and Learning | |
Planning under uncertainty | |
Plausibility | |
playground | |
plugin | |
polarity | |
polymorphism | |
polynomial approximation | |
polynomial calculus | |
polynomial closure | |
Polynomial functors | |
Polynomial Identity Testing | |
Polynomial Termination | |
polynomial time hierarchy | |
polynomial zonotopes | |
Portfolio | |
porting | |
POS tagging | |
positionality | |
Positive Almost Sure Termination | |
positivity | |
postulate-based reasoning | |
practical implementations | |
Practical Problem Solving | |
PRAM | |
pre-processing | |
Predicate Abstraction | |
preference based models | |
preferences | |
Preferential semantics | |
prefix unification | |
Premise Selection | |
preprocessing | |
Presburger | |
Presburger arithmetic | |
presentation | |
presentations | |
Preservation theorem | |
preserving primitivity | |
Presheaf Models of Type Theory | |
Priest's Logic of Paradox | |
Prime Implicants | |
prime implicates | |
primitive words | |
Principle-based Analysis | |
prioritized knowledge bases | |
privacy | |
Privacy Policy | |
privacy-utility trade-off | |
Private strategies | |
ProB | |
Probabilistic | |
probabilistic (affine additive) higher-order recursion schemes | |
Probabilistic Argumentation | |
probabilistic automata | |
Probabilistic Circuits | |
Probabilistic Graphical Models | |
probabilistic inference | |
Probabilistic Integer Programs | |
probabilistic lambda-calculus | |
Probabilistic Logic Programming | |
Probabilistic model checking | |
probabilistic process equivalences | |
probabilistic programming | |
Probabilistic programs | |
Probabilistic reasoning | |
probabilistic rewriting | |
probabilistic verification | |
probability | |
probability distribution | |
probability distributions | |
Probability logics | |
Probability Theory | |
Procedure | |
process algebra | |
process graphs | |
Process Mining | |
process modeling | |
Product Configuration | |
Productivity | |
program analysis | |
program distance | |
Program equivalence | |
Program Synthesis | |
program transformation | |
Program Verification | |
programming | |
Programming Errors | |
programming methodology | |
Progression | |
project management | |
Projected Model Counting | |
Projection | |
projective geometry | |
Prolog | |
Promise Constraint Satisfaction Problem | |
Promise Valued Constraint Satisfaction Problem | |
Proof | |
proof assistant | |
Proof assistants | |
proof automation | |
proof by reflection | |
proof checking | |
proof complexity | |
proof compression | |
Proof Discovery | |
proof engine | |
proof format | |
proof logging | |
proof methodology | |
Proof net | |
proof nets | |
proof presentation | |
proof representation | |
proof schemas | |
Proof search | |
proof structures | |
proof techniques | |
Proof theory | |
proof tree | |
proof-as-program | |
proof-search | |
Proof-search heuristics | |
Proofs | |
propagation | |
propagation redundancy | |
propagation redundant proof | |
propagation strength | |
Properties of Argumentation Semantics | |
property directed reachability analysis | |
Prophecy Variables | |
Proportional Representation | |
Propositional Dynamic Logic | |
propositional intermediate logics | |
propositional logic | |
Propositional planning | |
propositional proof complexity | |
propositional proof systems | |
Propositional satisfiability | |
propositional translations | |
Protege | |
protocol analysis | |
Protocol security | |
protocols | |
Protégé Plugin | |
Provenance | |
provenance semantics | |
Prover | |
Prover IDE | |
pseudo-Boolean constraints | |
Pseudo-Boolean optimization | |
pseudo-Boolean reasoning | |
pseudo-Boolean solving | |
Pseudo-contraction | |
pseudo-industrial random SAT | |
Psychology | |
PSyKE | |
Public Announcement Logic | |
Pure Type Systems | |
pushdown | |
PVS | |
python | |
Q | |
Q-resolution | |
QBF | |
QBF Programming | |
QBF proof complexity | |
QCDCL | |
QU-resolution | |
Qualitative Spatial Reasoning | |
Quantified Boolean Formula | (QBF2022) |
Quantified Information Flow | |
Quantified Integer Programming | (QBF2022) |
Quantified logics | |
Quantified modal logics | |
Quantified Optimization | (QBF2022) |
quantified reflection calculus | |
quantifier alternation | |
quantifier elimination | |
quantifiers | |
quantitative algebra | |
quantitative algebras | |
quantitative reasoning | |
Quantitative Synthesis | |
Quantitative theories | |
Quantitative types | |
Quantitative verification | |
quantitative/qualitative verification of omega-regular properties | |
Quantum Computation | |
Quantum computing | |
Quantum Decision Model | |
quantum information | |
Quantum Machine Learning | |
Quantum Noise | |
Quantum programming | |
Quantum random walk | |
Quantum weakest precondition | |
Quasicategories | |
Queries | |
query answering | |
Query Checking | |
query model | |
query optimization | (DL 2022) |
Query rewriting | |
query-by-example | |
Quillen equivalence | |
Quotient model | |
R | |
R1CS | |
Rabin automata | |
Ramsey quantifier | |
Random Descent | |
random Fourier features | |
random interpretations | |
random model | |
random numbers | |
Random quantities | |
Randomised Algorithms | |
randomization | |
Randomized Algorithms | |
randomized communication complexity | |
randomized computation | |
Randomized Planning | |
rank-width | |
ranking | |
Ranking Functions | |
rational closure | |
RDFS | |
reachability | |
Reachability analysis | |
reachability problem | |
Reactive synthesis | |
reactive systems | |
Realistic SAT generators | |
Realizability | |
Realizability Checking | |
Reasoning | |
Reasoning about action | |
Reasoning about action and change | |
Reasoning About Actions | |
Reasoning about Terminological Knowledge | |
rectangle decision lists | |
rectification | |
recurrent reachability | |
Recursion | |
Recursive path ordering | |
Reduction Measure | |
Reduction strategies | |
reduction-based systems | |
reductions | |
redundancy | |
Redundancy Elimination | |
Reed-Solomon coding | |
Reedy category | |
refactoring | |
Refactoring steps | |
refactoring tools | |
References | |
referring expressions | |
Refinement | |
Refutation calculus | |
Region Connection Calculus | |
Regression | |
Regular expressions | |
regular languages | |
Regular path queries | |
Regular Theories | |
Reimplication | |
reinforcement learning | |
relation extraction | |
relation-based explanations | |
Relational Queries | |
relaxation | |
relaxations | |
Relaxed Memory Models | |
Relay-based Railway Interlocking Systems | |
release engineering | |
relevance | |
Remez algorithm | |
replay attacks | |
replication | |
Requirements Analysis | |
research-based teaching | |
resolution | |
resolution complexity | |
Resolution over linear equations | |
resource approximation | |
Resource Description Framework with Schema (RDFS) | |
Resource Semantics | |
resource-constrained project scheduling problem | |
restricted probabilistic tree stack automata | |
Restricted Universal Variables | (QBF2022) |
restrictions | |
Results | |
reversal of list | |
reverse engineering | |
Reverse engineering of queries | |
reversible | |
Revision | |
revision postulates | |
rewriting | |
rewriting engines | |
rewriting induction | |
rewriting logic | |
Right barren | |
Robotics | |
Robots | |
robust safety | |
Robust solutions | |
Robustness | |
Robustness degree | |
Robustness Verification | |
roots of unity | |
Rota's basis conjecture | |
Rotations | |
Roth's Theorem | |
Rule Based | |
Rule based temporal action logic | |
Rule Based Theorem Provers | |
rule extraction | |
rule formats | |
rule learning | |
Rule Mining | |
rule-based reasoning | |
Rules as Code | |
run-time performance | |
runtime checking | |
Runtime Monitoring | |
runtime prediction | |
runtime-error verification | |
S | |
s(CASP) | |
Safe Autonomy | |
Safe Intelligent Control | |
Safe recursion | |
safety | |
sample complexity | |
sampling | |
SAT | |
SAT encodings | |
SAT modulo Symmetry (SMS) | |
SAT preprocessing | |
SAT Sampling | |
SAT solver | |
SAT solvers | |
SAT solving | |
SAT-based algorithms | |
SAT-solving | |
Satisfiability | |
Satisfiability Coding Lemma | |
Satisfiability Modulo Theories | |
Satisfiability Modulo Theory | |
satisfiability solving | |
Saturation | |
saturation-based theorem proving | |
Scenario optimization | |
Scheduling | |
SCL | |
search heuristic | |
Search space exploration |