GLOBAL TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
( | |
(iterated) admissibility | |
(Probabilistic) Integer Programs | |
- | |
- Data Mining | |
- High Utility Itemsets | |
- Propositional Satisfiability | |
0 | |
0-1 integer linear decision problem | |
0-1 laws | |
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 interpretation | |
Abstract machines | |
abstract rewriting | |
Abstract simplicial complexes | |
abstracted action models | |
abstraction | |
abstraction and refinement | |
abstraction refinement | |
Abstraction-Refinement | |
AC-Unification | |
Academic Career | |
Academic Environment | |
access control | |
Accessibility | |
Accountability | |
Accuracy | |
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 | |
Adjoint logic | |
Administrative Discretion | |
Adversarial Attacks | |
adversarial contexts | |
adversarial robustness | |
Adversarial Training | |
adversary argument | |
Advice | |
advisor | |
Aerospace | |
Agda | |
Agent autonomy | |
agent interrogation | |
agent programs | |
aggregates | |
Aggressive Bound Descent | |
AI | |
AI Certification | |
AI ethics | |
AI Safety | |
Airline scheduling | |
ALC | |
Algebra Interpretations | |
Algebraic Circuits | |
algebraic complexity | |
Algebraic Data Types | |
Algebraic Geometry | |
algebraic graph rewriting | |
algebraic hierarchy | |
Algebraic Measures | |
Algebraic Model Counting | |
algebraic number theory | |
algebraic proof systems | |
Algebraic reasoning | |
algebraic structures | |
Algorithm Portfolio | |
Algorithm Selection | |
Algorithmic Game Theory | |
algorithmic graph theory | |
Algorithms | |
all I know | |
Alloy | |
almost stable matching | |
almost-sat | |
alpha-equivalence | |
alphabetic equivalence | |
amalgamation property | |
Ambiguity | |
amortised cost analysis | |
analysis and design of cryptographic protocols | |
analytic tableaux | |
AND-OR graph | |
Angluin algorithm | |
Announcing KR2023 | |
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 | |
Applications of logic | |
Applied topology | |
Approval Voting | |
approximate counting | |
Approximate Reasoning | |
approximation | |
Approximation Fixpoint Theory | |
archery | |
Archive of Formal Proofs | |
argument mining | |
Argumentation | |
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 | |
ATP | |
Attack Trees | |
attacker advantage | |
attestation | |
auditable solving | |
authenticated encryption | |
authentication | |
Auto-Tuning | |
Autoencoding | |
Automata | |
automata theory | |
Automata-Theoretic Approach | |
automated algorithm configuration | |
automated algorithm design | |
Automated Deduction | |
automated deployment | |
automated driving | |
Automated ethics | |
automated grading | |
automated instance generation | |
automated numerical planning and scheduling | |
Automated planning | |
automated planning and scheduling | |
Automated proofs | |
automated reasoning | |
Automated Testing | |
automated theorem proving | |
Automated verification | |
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 | |
Aviation | |
Awards | |
axiom of choice | |
Axiomatic Systems | |
B | |
B\"uchi automata | |
back-and-forth method | |
back-translation | |
backdoor attack | |
backdoor depth | |
backdoor sets | |
Backdoors | |
Backreferences | |
Backtracking | |
Backtracking Search | |
Banach-Tarski | |
Bang calculus | |
Bar Recursion | |
Basic education | |
battle of Hercules and Hydra | |
Bayesian Machine Learning | |
Bayesian network classifiers | |
Bayesian Network Structure Learning | |
BCT | |
BDD | |
Behavioural equivalence | |
Belief | |
Belief Base | |
belief base change | |
Belief bases | |
belief change | |
Belief Contraction | |
Belief Fusion | |
Belief Merging | |
Belief Propagation | |
Belief Revision | |
belief update | |
Bell Labs | |
benchmarking | |
benchmarks | |
Bernays–Schönfinkel Fragment | |
Best paper award | (SAT) |
Best student paper award | (SAT) |
best-effort synthesis | |
Beth Definability Property | |
betterness relation | |
Beyond NP | |
bi-objective optimization | |
Biased graphs | |
Bicategories | |
bidirected | |
Big data | |
binary codes | |
Binary Constraint Tree | |
Binary Decision Diagrams | |
Biological Systems | |
bipolar argumentation | |
bisimilarity | |
bisimulation | |
bit pigeonhole principle | |
Bit-precise Reasoning | |
Bit-Vector Reasoning | |
Bit-vectors | |
blackboard | |
Blake Canonical Form | |
Block cipher modes | |
Block Ciphers | |
blockchain | |
Blockchains | |
blocked clauses | |
Boolean | |
Boolean algebra | |
Boolean algebras | |
boolean classifiers | |
boolean games | |
Boolean Network Synthesis | |
Boolean Satisfiability | |
Boolean 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-bound | |
branch-and-cut | |
branching bisimulation | |
Branching Time | |
Browser-based Applications | |
Bryant | |
Bug bounty | |
bug minimizer | |
Building Design | |
Building Information Modelling | |
Bunched Logic | |
bundled fragment | |
business meeting | |
Büchi automata | |
C | |
Cache | |
cache coherence | |
Calculus | |
Calculus of Names | |
Call by value | |
Call-by-name | |
call-by-push-value | |
Call-by-value | |
canonical structures | |
canonicity | |
canonization | |
capabilities | |
capability machines | |
Cardano | |
Cardinal Directional Calculus | |
Cardinality Constraints | |
career | |
case study | |
CASUAL | |
Catamorphisms | |
Categorial Robustness | |
Categorical model | |
Categorical models | |
categorical semantics | |
categories with families | |
Category | |
category theory | |
Cauchy integral formula | |
Cauchy-Goursat theorem | |
CAUSAL | |
Causal Bayesian Networks | |
causal graph | |
causal graphs | |
causal inference | |
causality | |
CAV | |
CBPV | |
CDCL | |
CDCL Algorithm | |
CDCL based Sampling | |
CDSAT | |
certificate checking | |
Certificates | |
certification | |
Certified Algorithms | |
certifying algorithms | |
certifying solvers | |
characterization | |
Chase termination | |
CHC | |
Checked C | |
cheminformatics | |
chi-boundedness | |
Choice logics | |
choice operator | |
Choice sequences | |
Choiceless Polynomial Time | |
chordal graphs | |
choreographies | |
choreography | |
Chu construction | |
Church encoding | |
Church's thesis | |
Chvátal-Gomory cuts | |
Ciao Prolog | |
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 proofs | |
clausal tableaux | |
Clause exchange | |
clause learning from simple models | |
clause redundancy | |
clause sharing | |
clique | |
clique-width | |
Closed Form | |
Closing | |
closure redundancy | |
Cloud Security | |
clustering | |
CNF | |
CNF Encoding | |
CNF translation | |
Co-stable Model Semantics | |
coalgebra | |
Cognitive Reasoning | (MC) |
Cognitive robotics | |
coherence | |
Coinduction | |
coinductive type | |
collaboration | |
collective attacks | |
Collective Entity Resolution | |
collusion-free protocols | |
collusion-preserving protocols | |
Color refinement algorithm | |
Coloring | |
Combination Problem | |
Combinations of Logic and Machine Learning | |
Combinations of Solvers and Gradient Descent | |
Combinatorial Enumeration | |
Combinatorial Inequalities | |
combinatorial optimisation | |
Combinatorial optimization | |
combinatorial proofs | |
combinatorial structures | |
Combinatorics | |
combinatorics on words | |
combinators | |
combinatory logic | |
combining decision procedures | |
Comment | |
commonsense knowledge | |
Commonsense reasoning | |
Commutation | |
Commutativity | |
comonads | |
compact closed categories | |
Comparators | |
compatibility | |
Competition | |
Competitions | |
compilation | |
compilation scheme | |
Compiler | |
compiler optimization | |
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 | |
complexity over structures | |
component based modeling | |
composite event recognition | |
Compositional Synthesis | |
Compositional Verification | |
compositionality | |
Compound conditionals | |
comprehensibility | |
Compressed tables | |
Computability | |
computability over structures | |
computability theory | |
Computable analysis | |
computable isomorphisms | |
computable queries | |
computational and-or graphs | |
computational aspects of argumentation | |
computational complexity | |
computational effect | |
computational interpretation | |
Computational Law | |
computational models of argument | |
Computational Security | |
computational social choice | |
Computer Algebra | |
Computer Science | |
Computer Science specialist | |
computer-aided cryptography | |
computer-assisted proof | |
computer-checked proofs | |
computing | |
Computing Education | |
computing explanations | |
Computing methodologies | |
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 rewriting | |
Conditional Term Rewriting Systems | |
Conditionals | |
Condorcet Jury Theorem | |
confidential computing | |
configuration language | |
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 | |
Consensus Protocols | |
consequence relations | |
conservative extensions | |
consistency | |
Consistency Analysis | |
Consistency Checking | |
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 logic programming | |
Constraint Modelling | |
Constraint Optimisation Problems | |
constraint optimization | |
Constraint Optimization Problems | |
constraint programming | |
constraint propagation | |
constraint satisfaction | |
Constraint Satisfaction Problem | |
constraint satisfaction problems | |
Constraint simplification | |
Constraint Solver | |
Constraint Solving | |
Constraint tableaux | |
Constraints | |
Constraints translation | |
constructive algebra | |
constructive matemathics | |
constructive mathematics | |
constructive type theory | |
Constructivity | |
Contamination Constraints | |
context-free expression | |
Context-free languages | |
Contextual equivalence | |
contextuality | |
continuous processes | |
continuous reachability | |
Contracts | |
contrastive explanations | |
control synthesis | |
Control-Flow Refinement | |
Controlled Natural Language | |
controlled natural languages | |
Controller Synthesis | |
convex polyhedra | |
convolutional autoencoders | |
Convolutional Neural Networks | |
Convolutional Neural Networks Verification | |
Cooperation in MAS | |
Cooperative agents | |
COPS#20 | |
copy-discard categories | |
Coq | |
Coq community | |
Coq library | |
coq plugin | |
Coq-Elpi | |
core extraction | |
corecursive function | |
correct-by-construction | |
correction sets | |
correspondence | |
COST | |
cost function network | |
Cost models | |
countably basic monad | |
counter automata | |
counter systems | |
Counterexamples | |
counterfactual explanations | |
Counterfactual Reasoning | |
Counterfactuals | (NMR) |
countermodel construction | |
counting | |
Counting Complexity | |
Counting Logics | |
Counting Proof Systems | |
Counting queries | |
Counting solutions | |
covert channels | |
CP-Logic | |
CPAchecker | |
CPSA | |
Craig interpolants | |
Craig interpolation | |
criteria | |
Critical Pair | |
Critical Pairs | |
CROWN | |
Crypto API | |
cryptographic protocol analysis | |
Cryptographic Protocol Shapes Analyzer (CPSA) | |
Cryptographic Protocols | |
cryptography | |
cryptosystem | |
CS education | |
CS-TRSs | |
CSP | |
CTL* | |
CTRSs | |
cube-and-conquer | |
cubical sets | |
Cubical Type Theory | |
curriculum | |
Curry-Howard | |
Curry-Howard correspondence | |
Cut Elimination | |
cut-elimination | |
cutting planes | |
Cyber-physical systems | |
cybersecurity | |
Cybersecurity and Fraud | |
cyclic dependencies | |
cyclic proof | |
Cyclic proofs | |
cyclicity | |
Cylindrical Algebraic Coverings | |
D | |
d-privacy | |
Darwiche-Pearl | |
Data analysis | |
Data Complexity | |
data federation | |
data graphs | |
data logics | |
Data Management | |
Data mining | |
Data Quality | |
data representation | |
Data Structures | |
Data Transfer | |
data words | |
data-driven algorithm design | |
Data-driven invariant learning | |
Data-driven methods | |
database dependencies | |
database query languages | |
database theory | |
Databases | |
databases as logical theories | |
dataflow programming | |
Datalog | |
Datalog rules | |
DatalogMTL | |
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 | |
declassification | |
decomposition | |
decreasing diagrams | |
Deducibility | |
Deductive Database Method | |
Deductive database method for geometry | |
deductive forgetting | |
deductive interpolation property | |
Deductive System | |
Dedukti | |
Deep Embedding | |
deep generative models | |
deep inference | |
deep learning | |
Deep Learning Compiler | |
Deep Neural Network Verification | |
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 | |
DeFi | |
definability | |
definable numbers | |
definite clause grammars | |
definite descriptions | |
definition by cases | |
Definition Variables | |
definitions | |
degrees of explainability | |
Delegate Reasoner | |
Denotational semantics | |
density | |
deontic cube | |
Deontic Logic | |
Dependency Analysis | |
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 | |
determinism | |
Deterministic Emerson-Lei automata | |
deterministic hierarchies | |
Determinization | |
development closed critical pairs | |
Diagonalizable matrices | |
Diagonalization porcedures | |
Diagrammatic language | |
Dial A Ride | |
Dial-A-Ride | |
dialectical explanations | |
Dialogue For Explanation | |
dichotomy theorem | |
Difference logic | |
difference logics | |
Differentiable Logic | |
Differential Categories | |
differential dynamic logic | |
Differential Linear Logic | |
differential privacy | |
Digital Forensics | |
Digital ICs | |
digraphs | |
Dijkstra commands | |
dimension theory | |
Dimensionality reduction | |
diophantine equations | |
diophantine sets | |
directed acyclic graphs | |
directed type theory | |
Discrete mathematics | |
Discrete Morse theory | |
discrete optimization | |
disjointness | |
disjunctive programs | |
Disjunctive Rules | |
Display calculus | |
distance bounding | |
distance bounding protocols | |
distant attacker | |
distributed algorithms | |
distributed automata | |
distributed ledger | |
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 | |
DNF | |
doctoral program | |
document stores | |
Domain Specific Languages | |
domain-specific language | |
domain-specific languages | |
Domains | |
dominance | |
Dominance Breaking | |
Dominance Relations | |
dot-depth hierarchy | |
double push out approach | |
double pushout approach | |
DP-3T | |
dpcp | |
DPRM theorem | |
DQBF | |
DQBF Solver | |
DRAT proofs | |
dual variables | |
dyadic deontic logic | |
Dynamic consistency checking | |
Dynamic Deontic Logic | |
Dynamic epistemic logic | |
Dynamic Logic | |
Dynamic Programming | |
dynamic release | |
dynamic symmetry breaking | |
Dynamics in Argumentation | |
E | |
E-unification | |
E-voting | |
EasyCrypt | |
Eckmann-Hilton | |
education | |
EELP | |
Effective algorithms | |
Efficient reasoning | |
Eisbach method | |
EKE | |
EL | |
EL ontologies | |
elaboration | |
elaborator reflection | |
Eldarica | |
elections | |
Electric power network | |
Electron | |
electronic voting | |
element-free probabilities | |
elementary computation | |
elementary functions | |
Elpi | |
Emaj-SAT | |
embarrassingly parallel search | |
Embedded systems | |
Embedding Space | |
Emerson-Lei acceptance | |
Emerson-Lei automata | |
emptiness | |
emulation | |
emv | |
encoding | |
Energy Efficiency | |
Enforcement | |
enriched monad | |
Ensembles | |
entailment | |
Entailment problem | |
Enthymemes | |
Entropy | |
Entropy Estimation | |
enumeration | |
envelope protocol | |
Epistemic Deontic Logic | |
epistemic logic | |
Epistemic Logics | |
Epistemic State | |
Epistemic States | |
epistemic uncertainty | |
equational logic | |
equational theories | |
equational unification | |
equivalence | |
Equivalence checking | |
Equivalence Prover | |
Equivalence Verification | |
Erlang | |
Ethereum | |
Ethereum 2.0 | |
Ethical Reasoning | |
Ethics | |
Euclidean Geometry | |
EuroProofNet | |
evaluation | |
evaluation order | |
Event Calculus | |
Events | |
Eventual non-negativity | |
everybody | |
Evolution | |
Ewens distribution | |
exact computation | |
Exact Learning | |
exclusion set | |
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 | |
extended resolution | |
Extensional Type Theory | |
F | |
F* | |
factor interpretation | |
fair exchange | |
Fair simulation | |
fairness | |
Fairness Verification | |
fallacious argumentation | |
Fallible sensors | |
Farkas' Lemma | |
fault isolation | |
feasible fragments | |
feature extraction | |
federated data trading | |
feedback | |
fibrations | |
Filtering algorithm | |
Fine-grained Access Control | |
fine-grained locking | |
finite abstraction | |
finite automata | |
finite axiomatizability | |
finite constraint languages | |
Finite entailment | |
finite fields | |
Finite Model Theory | |
finite models | |
Finite-state abstractions | |
finite-variable logics | |
finitely basic monad | |
finitely subdirectly irreducible | |
finiteness | |
fintech | |
firmware | |
First-order | |
first-order ATP | |
first-order logic | |
First-order logic with equality | |
First-order LTL | |
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-Point | |
Floating-Points | |
fluted fragment | |
FO model checking | |
Focused proof systems | |
FOL | |
FOL= | |
Forecasting | |
Forgetting | |
forgetting tools | |
Formal | |
formal argumentation | |
formal languages | |
formal logic | |
formal mathematics | |
formal methods | |
formal methods and verification | |
formal modeling | |
Formal Models | |
formal proof | |
Formal Proof Techniques | |
formal proofs | |
formal semantics | |
Formal specification | |
formal verification | |
formalization | |
formalization of category theory | |
formalization of mathematics | |
formula | |
Formula Simplification | |
formulas | |
Foundations | |
Foundations of Mathematics | |
Foundations of Programming | |
Frank Pfenning | |
free algebras | |
free-choice nets | |
Frequency Moments | |
Full-angle Method | |
full-system guarantees | |
Function algebras | |
Function Symbols | |
functional analysis | |
functional big-step semantics | |
Functional Causal Models | |
Functional correctness verification | |
Functional Data Structures | |
Functional logic programming | |
Functional Machine Calculus | |
Functional programming | |
Functional Properties | |
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 | |
game comonads | |
Game semantics | |
game theory | |
games | |
games on graphs | |
gang membership | |
Garbage Collection | |
Gauge integral | |
Gauss-Jordan Elimination | |
Gaussian elimination | |
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 | |
geometric logic | |
Geometry automated theorem provers | |
Geometry Problem Solving | |
Georg Cantor | |
Gini index | |
Giuseppe Peano | |
global constraints | |
gluing | |
Goal-Directed | |
Goal-Directed Answer Set Programming | |
Goal-Directed evaluation | |
goal-oriented proof system | |
Goals | |
Godel's Completeness Theorem | |
GPU | |
GQL | |
Graded logic | |
graded modalities | |
Graded monads | |
Gradual Argumentation | |
gradual semantics | |
grammar-based tree compression | |
graph | |
graph coloring | |
Graph databases | |
Graph games | |
graph grammar | |
graph isomorphism | |
Graph Neural Networks | |
graph node property prediction | |
graph partitioning | |
graph queries | |
graph query languages | |
graph rewriting | |
graph theory | |
graph transformations | |
Graph-minors | |
graphical calculus | |
graphical feedback | |
graphical language | |
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 | |
H | |
hardware | |
hardware tokens | |
Hardware Verification | |
Haskell | |
Herbrand Semantics | |
Heterogeneous knowledge bases | |
heuristic algorithms | |
Heuristic function construction | |
heuristics | |
Hierarchical Models | |
High School Students | |
High-assurance communication | |
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 programs | |
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 Clause Solving | |
Horn formula | |
Horn theories | |
Horn-DL | |
Horn-fragments | |
HTN Planning | |
human cognition | |
human computer interaction | |
human reasoning | |
Human-Aware AI | |
Human-Computer Interaction | |
Human-robot collaboration | |
Hybrid AI | |
Hybrid Knowledge Bases | |
Hybrid Logic | |
Hybrid MKNF Knowledge Bases | |
Hybrid planning | |
Hybrid Programs | |
hybrid reasoning | |
hybrid systems | |
Hyper-parameter optimisation | |
Hyper-parameters tuning | |
hyperdoctrine | |
hyperintensionality | |
Hyperliveness | |
HyperLTL | |
Hyperproperties | |
Hypersequents | |
I | |
iALC | |
identity management | |
Imandra | |
Imperative language | |
imperative program | |
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 | |
incomplete information | |
incompleteness | |
inconsistency-tolerant semantics | |
incremental CDCL | |
incremental MaxSAT | |
incremental SAT | |
Incremental SAT Solving | |
Independent Hashing | |
Indistinguishability | |
induction | |
Induction and coinduction | |
Inductive inference | |
inductive inference operator | |
Inductive Logic Programming | |
Inductive reasoning | |
inductive theorem proving | |
industrial research | |
Industry | |
infeasibility | |
inference schemas | |
infinite duration | |
infinite proofs | |
infinite stable models | |
infinite-domain constraint satisfaction problem | |
infinite-state systems | |
infinity-topos | |
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 | |
Interaction | |
Interactive Explanations | |
interactive textbook | |
Interactive Theorem Proving | |
Interactive Verification | |
Interactive Web System | |
Interdisciplinary reasearch | |
Interference-based proofs | |
Intermediate conditions and effects | |
Intermediate Logics | |
internal language | |
Internet of Things | |
Interpolation | |
Interpretability | |
interpretable models | |
Interpretable prediction | |
Interpretation | |
interpretation of sparse graphs | |
interpretations | |
Intersection Types | |
introduction | |
Intuitionism | |
intuitionistic linear logic | |
intuitionistic logic | |
Invariance | |
Invariant synthesis | |
invertibility | |
Invited Talk | |
Iris | |
ISA specification | |
Isabelle | |
Isabelle Proof Assistant | |
Isabelle Sledgehammer | |
Isabelle/HOL | |
Isabelle/jEdit | |
Isabelle/VSCode | |
isolation problem | |
isomorph-free exhaustive generation | |
isomorph-free 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-consistency | |
k-SAT | |
KALM | |
Kan-Quillen model structure | |
Kant | |
Kavraki | |
Kemeny Rank Aggregation | |
Kernel Contraction | |
kernelization | |
key agreement | |
key exchange | |
key hierarchy | |
Key management | |
keyword1 | |
keyword2 | |
keyword3 | |
Kleene Algebra | |
Kleene star | |
knapsack | |
knowability | |
Knowledge | |
Knowledge Acquisition | |
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 | |
Kochen–Specker systems | |
Kolmogorov complexity | |
Koopman operator | |
kr | |
KR and Machine Learning | |
KR2022 | |
Kripke semantics | |
Kupferman | |
L | |
L.E.J. Brouwer | |
Labelled Tableaux | |
Labelled Transition Systems | |
Lafont category | |
lambda calculus | |
lambda-abstraction | |
lambda-calculus | |
lambda-mu-calculus | |
lambda-pi calculus modulo theory | |
Lambek calculus | |
language | |
Language inclusion | |
language minimalism | |
Language of a knowledge base | |
language-based mechanisms | |
language-based security | |
languages | |
large neighborhood search | |
Large Neighbourhood Search | |
Large Prime Fields | |
Large-Neighbourhood Search | |
LARS | |
lattice theory | |
law enforcement | |
Law of Excluded Middle | |
laws | |
Layered Attestation | |
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 | |
Learning-enabled systems | |
Least General Generalizations | |
ledger | |
ledger model | |
Legal Contracts | |
Legal Reasoning | |
Legal Rule Modelling | |
Legal Technology | |
Legendre PRF | |
lemma generation | |
Letrec languages | |
lex modality | |
lexicographic inference | |
Leximax | |
LF | |
library | |
library design | |
Library of encodings | |
life sciences | |
Lifted Inference | |
lifted strips | |
Limit-Deterministic Buchi Automata | |
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 | |
Linear Time Logic | |
Linear Time Logic on Finite Traces | |
Linear-time Temporal Logic on Finite and Infinite Traces | |
Linear-time/branching-time spectrum | |
Linearisation | |
linearize arithmetic | |
Linicrypt | |
Linkability | |
linter | |
list | |
literate programming | |
Liveness | |
LLVM | |
lob induction | |
Local associativity | |
local consistency | |
local deduction theorem | |
Local robustness | |
Local Search | |
local verification | |
local-time semantics | |
Locality | |
locally bounded treewidth | |
locally presentable category | |
Log Generation | |
Logarithmic Space | |
Logic | |
Logic and finite model theory | |
Logic and Law | |
logic at school | |
logic course | |
logic curricula | |
logic for beginners | |
Logic for CS | |
logic for PTime | |
logic in computer science | |
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 | |
Logical theories | |
Logics for Multi-Agent Systems | |
Logics for the strategic reasoning | |
Lookaheads | |
loop acceleration | |
Loop Invariant Generation | |
Loop termination | |
Loss Functions | |
losslessness | |
Lossy channel systems | |
Low-complexity Description Logics | |
lower bound | |
lower bounds | |
lower runtime bounds | |
Lower-regular | |
LP | |
LP^MLN | |
LREC | |
LTI | |
LTL | |
LTL model checking | |
LTL over finite traces | |
LTLf | |
LTLf synthesis | |
M | |
machine learning | |
machine learning classifiers | |
Machine Learning Compiler | |
machine learning theory | |
Machine Reasoning | |
magic wand | |
maintainability | |
mandatory security policies | |
Manufacturing | |
Many-Sorted Logic | |
MAP inference | |
Marabou | |
Marine Exploration | |
Maritime Traffic Control | |
Markdown | |
Markov categories | |
Markov decision processes | |
Markov equivalence | |
Markov Logic Networks | |
Martingales | |
masking | |
Match-bounds | |
Matching | |
matching modulo AC | |
Mathematical Components | |
Mathematical Formalisation | |
mathematical intuition | |
Mathematical Knowledge Exploration | |
Mathematical Learning Environment | |
mathematical logic | |
mathematical programming | |
mathematical proofs | |
Mathematics | |
Mathematics Education | |
Mathematics of computing | |
mathlib | |
Matrix Algebra | |
matroid | |
Max#SAT | |
Max-CSP | |
max-sat | |
Max-SAT Resolution | |
maximum clique | |
maximum satisfiability | |
MaxSAT | |
Mazurkiewicz Traces | |
MC Competition | |
MDD | |
Mean payoff | |
mean payoff games | |
measure theory | |
Mechanism Design | |
mechanization | |
Mechanized Logic | |
mechanized proofs | |
membership | |
membership inference | |
Memory allocation | |
Memory automata | |
memory sharing | |
Mentoring | |
message passing | |
Meta Logic Solving | |
meta-programming | |
Meta-theory | |
Metaheuristics | |
metric differential privacy | |
metric spaces | |
metric temporal queries | |
metrics | |
Minimal Independent Sets | |
Minimal Modification | |
Minimal tableau | |
Minimal typings | |
minimal unsastisfiable set | |
Minimalist Type Theory | |
minimality criterion | |
Minimally Unsatisfiable Subsets | |
Minimum description length | |
minimum explanations | |
minimum hitting sets | |
misconceptions | |
Mixed Integer Progamming | |
Mixed Integer Programming | |
Mixed-Integer Programming | |
Mizar | |
MKNF | |
MLTL | |
modal logic | |
Modal logics | |
modal mu-calculus | |
modal operators | |
modal type theory | |
modalities | |
model building | |
model checking | |
Model Checking Problem | |
Model completion | |
Model Counter | |
model counting | |
model finding | |
model learning | |
Model reconciliation | |
Model Synthesis | |
model theory | |
model-based reasoning | |
Model-Checking | |
Model-Free Reinforcement Learning | |
Modeling | |
Modelling | |
models of computation | |
Modern AI | |
modular circuits | |
modular reasoning | |
Modular termination | |
modularity | |
Module checking | |
module system | |
monadic decomposability | |
monadic dependence | |
monadic embedding | |
monadic NP | |
monadic second-order logic | |
monadic stability | |
monads | |
monoidal category | |
monoidal closed categories | |
monoidal stream | |
monoidal width | |
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 Path Finding | |
Multi-Agent Systems | |
Multi-Agent Systems (MAS) | |
Multi-context systems | |
Multi-homomorphism | |
Multi-Layer Modification | |
multi-modal verification | |
Multi-Objective Optimisation | |
Multi-objective optimization | |
multi-paradigm | |
Multi-shot solving | |
Multi-Threaded Solving | |
multi-valued decision diagrams | |
Multilayer Perceptrons | |
multinomial theorem | |
multiparty communication complexity | |
multiparty computation | |
Multiplicative-additive fragment | |
multiplier verification | |
multiset | |
multiset rewriting | |
multistep reduction | |
Multiwinner Voting | |
muMALL | |
music composition | |
Music generation | |
mutation | |
Mutation Testing | |
N | |
Narrowing strategies | |
Nash Equilibria | |
Natural Deduction | |
natural language generation | |
natural language processing | |
Natural Language Understanding | |
natural semantics | |
Negation as Failure | |
Negative Statements | |
Negative tables | |
negative translation | |
negotiations | |
nested regular path queries | |
Nested sequent | |
Nested sequent calculus | |
network security | |
Networks | |
networks/graphs | |
neural language models | |
Neural network | |
Neural Network Compression | |
Neural Network Equivalence | |
Neural Network Models | |
Neural Network Modification | |
neural network robustness | |
Neural Network Verification | |
Neural Networks | |
Neural networks verification | |
neural symbolic artificial intelligence | |
Neural-symbolic integration | |
Neuro-Symbolic | |
neuro-symbolic AI | |
neuro-symbolic computing | |
neuro-symbolic reasoning | |
Neuronal networks | |
Neurosymbolic AI | |
NFA | |
NFA/MDD constraint | |
NLP | |
NMatrices | |
Node-RED | |
nominal algorithms | |
nominal logic | |
Nominal Techniques | |
Non-classical Logic | |
non-classical logics | |
Non-classical Semantics | |
Non-deterministic Semantics | |
non-interactive key exchange | |
Non-linear Arithmetic | |
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-standard logic | |
non-termination | |
Nondeterminism | |
Nondisjoint theories | |
noninterference | |
nonlinear real arithmetic | |
nonmonotonic reasoning | |
Nonstandard Logic | |
Normal Logic Programs | |
Normalisation | |
normalization | |
normalization by evaluation | |
Normalized Edit Distance | |
Normative Systems | |
notebook | |
nowhere dense | |
Nullstellensatz | |
Number Fields | |
Numerical Analysis | |
numerical-optimization search | |
O | |
OBDA | |
OBDD | |
OBDD-based proof systems | |
Object-Centric Event Logs | |
observational equivalence | |
off-chain channels | |
off-line guessing | |
Omega Automata | |
OMQA | |
onion address | |
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 |