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-ﬂow 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 |