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 | |
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 game semantics | |
operational semantics | |
operator | |
Optimal ABox Repair | |
optimal proof systems | |
optimisation | |
optimization | |
Optimization Algorithms | |
optimization modulo theory | |
orbit-finite sets | |
Order-Sorted Logic | |
Ordered Disjunction | |
Ordered Local Confluence | |
Ordered Multivalued Decision Diagram | |
Ordinal Conditional Functions | |
ordinary differential equations | |
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 Reasoning | |
Parallel Sorting Algorithms | |
parallel-innermost rewriting | |
Parallelizing transformations | |
Parameter learning | |
parameterised Boolean equation systems | |
parameterized complexity | |
Parametric continuous-time Markov chains | |
parametric solution | |
paramodulation | |
pareto front enumeration | |
Parity automata | |
parity games | |
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 | |
PB solving | |
PBPO+ | |
PCTL | |
PDF.js | |
Peano arithmetic | |
pebble-relation | |
pedagogy | |
Perception & Reasoning | |
perfect matching | |
performance | |
performance prediction | |
Permitted Announcements | |
permutation equivalence | |
Personal Advice | |
Personal Experience | |
Personal Lessons | |
Perspectives | |
petri nets | |
phase distinction | |
Physical observable | |
physical properties | |
pi-calculus | |
pi-forall | |
Pigeonhole principle | |
Plan execution monitoring | |
Planning | |
Planning and Learning | |
Planning under uncertainty | |
Plausibility | (MC) |
play-off competitions | |
plugin | |
Poisoning attacks | |
polarity | |
polymorphism | |
polynomial approximation | |
polynomial calculus | |
polynomial closure | |
Polynomial functors | |
Polynomial Identity Testing | |
polynomial termination | |
polynomial time hierarchy | |
polynomial zonotopes | |
popularization paper | |
Portfolio | |
Portfolio parallel SAT solver | |
portfolios | |
porting | |
POS tagging | |
positionality | |
Positive Almost Sure Termination | |
positivity | |
postulate-based reasoning | |
power side channels | |
practical implementations | |
Practical Problem Solving | |
PRAM | |
pre-processing | |
Precision | |
Predicate Abstraction | |
preference based models | |
preferences | |
Preferential semantics | |
prefix unification | |
Premise Selection | |
Preorders | |
preprocessing | |
PRES+ model | |
Presburger | |
Presburger arithmetic | |
presentation | |
presentations | |
Preservation theorem | |
preserving primitivity | |
Presheaf Models of Type Theory | |
pricing mechanism | |
Priest's Logic of Paradox | |
Prime Implicants | |
prime implicates | |
primitive words | |
principle-based analysis | |
prioritized knowledge bases | |
Privacy | |
Privacy Policy | |
Privacy-Preserving Machine Learning | |
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 | |
Probabilities | |
probability | |
probability distribution | |
probability distributions | |
Probability Theory | |
Procedure | |
process algebra | |
process graphs | |
Process Mining | |
process modeling | |
Product Configuration | |
productivity | |
Professionalism | |
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 | |
Projectivitiy | |
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 of unsatisfiability | |
proof presentation | |
Proof Production | |
proof representation | |
proof schemas | |
Proof search | |
proof structures | |
proof techniques | |
proof theory | |
Proof transformation | |
proof tree | |
proof-as-program | |
proof-search | |
Proof-search heuristics | |
proofgold | |
Proofs | |
propagation | |
propagation redundancy | |
propagation redundant proof | |
propagation strength | |
Properties of Argumentation Semantics | |
Property Based Testing | |
property directed reachability analysis | |
property language design | |
Property-Based Testing | |
Prophecy Variables | |
Proportional Representation | |
Propositional Dynamic Logic | |
propositional intermediate logics | |
propositional logic | |
Propositional planning | |
propositional proof systems | |
Propositional satisfiability | |
Protege | |
protocol analysis | |
protocol logic | |
Protocol security | |
Protocol verification | |
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 | (MC) |
PSyKE | |
Public Announcement Logic | |
Pure Type Systems | |
pushdown | |
PVS | |
Python | |
Python Scikit-learn | |
Q | |
Q-resolution | |
QBF | |
QBF Competition | |
QBF Programming | |
QBF proof complexity | |
QCDCL | |
QPTIME | |
QU-resolution | |
Qualitative Spatial Reasoning | |
quantified | |
Quantified Boolean Formula | |
Quantified Information Flow | |
Quantified Integer Programming | |
Quantified logics | |
Quantified modal logics | |
Quantified Optimization | |
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 mechanics | |
Quantum Noise | |
quantum programming | |
Quantum random walk | |
Quantum weakest precondition | |
Quasicategories | |
Queries | |
query answering | |
Query Checking | |
Query Evaluation | |
query model | |
query optimization | |
Query rewriting | |
query-by-example | |
Quillen equivalence | |
Quotient model | |
R | |
R1CS | |
Rabin automata | |
Racket | |
Ramsey quantifier | |
Random Descent | |
Random Forest Classifier | |
random Fourier features | |
random interpretations | |
random model | |
random numbers | |
Random quantities | |
Randomised Algorithms | |
randomization | |
Randomized Algorithms | |
randomized communication complexity | |
randomized computation | |
Randomized Planning | |
Randomized Synthesis | |
rank width | |
rank-width | |
Ranking Functions | |
rational closure | |
Rational Functions | |
Rational Synthesis | |
rationality | |
RDFS | |
reachability | |
Reachability analysis | |
reachability problem | |
reactive synthesis | |
Reactive systems | |
real domain | |
Realistic SAT generators | |
Realizability | |
Realizability Checking | |
Reasoning | |
Reasoning about action | |
Reasoning about action and change | |
reasoning about actions | |
Reasoning about Terminological Knowledge | |
Reasoning Systems | |
Recollections | |
reconfigurable interaction | |
rectangle decision lists | |
rectification | |
recurrent reachability | |
Recursion | |
Recursive path ordering | |
Recursive program | |
Reduction Measure | |
Reduction strategies | |
reduction-based systems | |
reductions | |
redundancy | |
Redundancy Elimination | |
Reed-Solomon coding | |
Reedy category | |
Reentrancy Attack | |
refactoring | |
Refactoring steps | |
refactoring tools | |
References | |
referring expressions | |
Refinement | |
Refutation calculus | |
Region Connection Calculus | |
Register automata | |
Regression | |
Regular expressions | |
regular languages | |
Regular path queries | |
Regular Theories | |
Reimplication | |
reinforcement learning | |
relation extraction | |
relation-based explanations | |
relational complexity | |
relational databases | |
relational machines | |
Relational Queries | |
relaxation | |
relaxations | |
Relaxed Memory Models | |
Relay-based Railway Interlocking Systems | |
release engineering | |
Relevance | |
Remez algorithm | |
remote attestation | |
Remote debugging | |
Repair of Neural Networks | |
replay attacks | |
replication | |
representation learning | |
Reproducible parallel SAT solving | |
Requirements Analysis | |
Research Career | |
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 | |
restrictions | |
Results | |
reversal of list | |
reverse engineering | |
Reverse engineering of queries | |
reversible | |
Revision | |
revision postulates | |
rewriting | |
rewriting engines | |
rewriting induction | |
rewriting logic | |
Right barren | |
RNN | |
Robotics | |
Robots | |
Robust Compression | |
robust safety | |
Robust Solutions | |
Robustness | |
Robustness degree | |
robustness verification | |
Ron Fagin | |
roots of unity | |
Rota's basis conjecture | |
Rotations | |
Roth's Theorem | |
RSS | |
Rule Based | |
Rule based temporal action logic | |
Rule Based Theorem Provers | |
rule formats | |
rule learning | |
Rule Mining | |
rule-based reasoning | |
Rules as Code | |
Run-time checks | |
Run-time enforcement | |
run-time performance | |
runtime checking | |
Runtime Monitoring | |
runtime prediction | |
Runtime verification | |
runtime-error verification | |
S | |
s(CASP) | |
Safe Autonomy | |
Safe Intelligent Control | |
Safe recursion | |
safety | |
sample complexity | |
sampling | |
SAT | (SAT) |
SAT competition | |
SAT encodings | |
SAT modulo Symmetry (SMS) | |
SAT preprocessing | |
SAT Sampling | |
SAT solver | |
SAT solvers | |
SAT solving | |
SAT-based algorithms | |
SAT-based reasoning | |
SAT-solving | |
Satisfiability | |
satisfiability checking | |
Satisfiability Coding Lemma | |
Satisfiability Modulo Theories | |
Satisfiability Modulo Theory | |
Satisfiability Solvers | |
satisfiability solving | |
Saturation | |
saturation-based theorem proving | |
Scenario optimization | |
Schedulers | |
scheduling | |
SCL | |
SDD | |
search heuristic | |
Search methodologies | |
Search space exploration | |
SeCaV | |
Second-Order Arithmetic | |
second-order equations | |
secure bandwidth allocation | |
secure blockchain | |
secure compilation | |
secure locatization protocols | |
Secure Multi-Party Computation | |
secure protocols | |
Secure voting systems | |
security | |
Security Policy | |
security protocols | |
Security Verification | |
Selene | |
self-adjusting data structures | |
self-authentication | |
Selfie attack | |
SELinux | |
Semantic | |
semantic forgetting | |
Semantic policies | |
semantics | |
semantics of programming languages | |
semi-deterministic automata | |
Semidefinite programming | |
semilinear | |
semilinear sets | |
semiring semantics | |
semirings | |
semistrict | |
Sentence Embeddings | |
Sentential Decision Diagram | |
separated relations | |
separation | |
Separation Logic | |
separations | |
sequence generation | |
Sequence Variables | |
Sequences of probability distributions | |
sequencing | |
Sequent Calculi | |
Sequent Calculus | |
sequent-based argumentation | |
sequentiality | |
Sequentialization | |
Series-parallel graphs | |
series-parallel orders | |
Service robotics | |
Session types | |
set theory | |
sets with atoms | |
SGGS | |
shallow embedding | |
Shannon Entropy | |
shared memory | |
Sharing | |
sharing economy | |
sheaf cohomology | |
sheaves and cohomology | |
Sherali-Adams | |
Ship refit planning | |
shrubdepth | |
Shy Datalog+/- | |
Sigma-monoid | |
signal flow graph | |
Signal temporal logic | |
Simplicial homology | |
simplicial type theory | |
Simulated Annealing | |
simulation | |
simulations | |
situation calculus | |
sized types | |
Skolem | |
Skolem Conjecture | |
Skolem Problem | |
Sledgehammer | |
slides | |
smart contract | |
Smart Contracts | |
Smart Devices | |
smart-contracts | |
SMT | |
SMT callbacks | |
SMT solvers | |
SMT Solving | |
SMT-LIB | |
SMT-solvers | |
Social Choice | |
software bounded model checking | |
software development | |
software engineering | |
software independence | |
software reliability | |
Software Synthesis | |
software verification | |
Solidity | |
Solution counting | |
solution reconstruction | |
solution-improving search | |
Solvability | |
Solver Competition | |
solver engine | |
solver portfolios | |
solvers | |
Solving | |
Sorting Networks | |
sound and complete calculus | |
soundness | |
Space complexity | |
Spatial Memory Safety | |
Special event | |
special session | |
Species Interaction Code | |
Species of structures | |
Specification | |
Spread constraint | |
SSAT | |
stability | |
Stable Model Semantics | |
stable models | |
stable roommates problem | |
Stable-Unstable Semantics | |
Standard | |
Standpoint | |
Stanza | |
state machines | |
static analysis | |
Static equivalence | |
Static Program Analysis | |
Statistical Model Checking | |
Statistical relational artificial intelligence | |
Statistical Relational Learning | |
Statistical Statements | |
Statistical Verification | |
statistics | |
steering | |
stochastic actions | |
Stochastic Approximation | |
Stochastic Arithmetic | |
Stochastic Boolean Satisfiability | |
stochastic constraints | |
stochastic game | |
Stochastic games | |
Stochastic invariants | |
stochastic logic programming | |
stochastic process | |
Stochastic Processes | |
stochastic systems | |
Straight-line programs | |
strand spaces | |
Strategic Reasoning | |
strategies | |
strategy extraction | |
Strategy Logic | |
strategy scheduling | |
Straubing conjecture | |
stream | |
stream reasoning | |
strict units | |
strictly positive logic | |
String constraints | |
string diagrams | |
String rewriting | |
string-diagrammatic semantics | |
Strings | |
strong bisimulation | |
Strong Equivalence | |
strong persistence | |
Strongly Connected Components | |
Strongly Connected Components (SCCs) | |
structural induction | |
Structural operational semantics | |
structural parameters | |
structural soundness | |
structure | |
structured argumentation | |
Structured editor | |
structured proofs | |
Subexponentials | |
Subgraph isomorphism | |
suboptimal planning | |
substitution | |
Subsumption | |
Subword order | |
Sufficient Reasons | |
sum-of-squares | |
summer school | |
superposition | |
Superposition Reasoning | |
Support Vector Machine | |
survey | |
surveys | |
Survival of the Fitted | |
Sweedler dual | |
syllepsis | |
symbolic bisimulation | |
Symbolic Computation | |
Symbolic Execution | |
symbolic knowledge extraction | |
Symbolic Model Checking | |
symbolic reachability | |
symbolic security analysis | |
symbolic verification | |
symbolic vs. neural AI | |
symmetric choice | |
Symmetric fractional polymorphisms | |
Symmetric key cryptography | |
symmetries | |
symmetry breaking | |
Symmetry Breaking Constraints | |
symmetry detection | |
Synchronization | |
syntax splitting | |
syntax with bindings | |
Synthesis | |
Synthesis under Environment Specifications | |
synthetic computability | |
synthetic computability theory | |
Synthetic domain theory | |
synthetic probability | |
Synthetic tableau | |
synthetic Tait computability | |
system description | |
System W | |
systems engineering | |
Szemerédi's Regularity Lemma | |
T | |
tableau algorithm | |
Tableau algorithms | |
Tableaux | |
tactic | |
tagged architectures | |
Talks | |
tansfer package | |
Task planning | |
Taylor expansion | |
TBA | |
TBA1 | |
TBA2 | |
TBA3 | |
TBD | |
teaching | |
teaching automated reasoning | |
Teaching Logic | |
teaching support system | |
teaching support systems for logic | |
Team Semantics | |
temporal abstraction | |
Temporal Data | |
Temporal Logic | |
Temporal Logics | |
temporal pattern matching | |
Temporal planning | |
Temporal Queries | |
temporal reasoning | |
temporally-constrained effects of events | |
Tennenbaum's theorem | |
term modal logic | |
term orderings | |
Term representation | |
Term Rewrite Systems | |
term rewriting | |
TermComp | |
Termination | |
Termination Competition | |
Ternary satisfaction relation | |
Test Case Generation | |
Testing | |
Testing of Samplers | |
text graphs | |
Text-based Games | |
The Art of Computer Programming | |
The General Schema | |
The MITRE Corporation | |
Theorem prover | |
Theorem prover soundness | |
theorem provers for intuitionistic propositional logic | |
theorem proving | |
theorem synthesis | |
theories | |
theory of changes | |
Theory of Heaps | |
Theory of intentions | |
Theory of Sequences | |
theory reasoning | |
three-dimensional stable matching with cyclic preferences | |
Three-valued Logic | |
threshold automata | |
Threshold operators | |
thunk-force categories | |
time | |
Time Management | |
Time-granularity | |
Time-Sensitive Distributed Systems | |
timed automata | |
TLS Certificates | |
to | |
toasts | |
Tool | |
Tool framework | |
tools | |
Tools for Teaching Logic | |
Top-down proof procedure | |
Topics | |
topological multisorting | |
topological semantics | |
topology | |
topos theory | |
Tournament Fixing problem | |
TPTP | |
TPTP World | |
trace graph | |
Tractable Probabilistic Models | |
tractable reasoning | |
Trail saving | |
Training Deep Neural Networks | |
Trajectory Learning | |
transducers | |
transduction | |
transductions | |
transformation | |
Transition system | |
transition systems | |
Transitive Closure Logic | |
translation | |
Translation validation | |
Transmission maintenance scheduling | |
Transport Layer Security | |
tree automata | |
Tree decomposition | |
tree grammar | |
tree search | |
tree width | |
tree-like proofs | |
treedepth | |
Treewidth | |
Treewidth-aware reductions | |
Trigger-Action Platform (TAP) | |
TRSs | |
trust | |
trustworthy AI | |
trustworthy decision making | |
Truth-tracking | |
Tseitin | |
Tseitin formulas | |
TSPTW | |
tuple interpretations | |
tuple-generating dependency | |
Turan number | |
Turing Complete | |
tutorial | |
twin-width | |
two level type theory | |
Two-dimensional logics | |
Two-level approach | |
Two-player games | |
two-variable first-order logic | |
two-variable fragment | |
two-watched literal scheme | |
type classes | |
type inference | |
type refinement | |
type systems | |
type theory | |
type universes | |
type-based termination | |
Typicality | |
Typicality in Description Logics | |
Türing Machine | |
U | |
UAV Compliance Checking | |
unary uninterpreted predicates | |
Uncertainty | |
Uncertainty Reasoning | |
Undecidability | |
Underapproximation widening | |
undergraduate | |
undergraduate mathematics | |
unforgeable pointers | |
unification | |
Unification in Description Logics | |
unification theory | |
Unified Payment Interface | |
Uniform equivalence | |
Uniform Random Sampling | |
Uniform Sampling | |
unifying framework | |
UniMath | |
Unique Characterizablity | |
univalence | |
Univalent Foundations | |
universal contracts | |
universal graphs | |
universal optimality | |
unlinkability | |
unsatisfiable | |
unsatisfiable cores | |
Unsatisfiable Subset Optimization | |
Unstructured Data | |
unsupervised learning | |
up-to techniques | |
update postulates | |
Upper and Lower Bounds | |
upper bound | |
upper runtime bounds | |
user authorization query problem | |
user benchmark | |
User interface | |
User interfaces | |
user studies | |
User study | |
UTXO | |
V | |
Vadalog | |
value iteration | |
Vardi | |
Vardifest | |
Variable Neighborhood Search | |
Variable Ordering Heuristic | |
VC dimension | |
vector addition systems | |
Vehicle Routing | |
vehicular platooning | |
Verifiable voting systems | |
Verification | |
verification conditions | |
verification infrastructures | |
Verification of Complex Systems | |
verification of hybrid systems | |
verification of neural networks | |
verification of probabilistic programs | |
Verified compilation | |
Verified Numerics | |
Verified Software Toolchain | |
Version space algebras | |
view-based query answering | |
view-based query processing | |
Virtual Knowledge Graph | |
virtual machines | |
Visual programming | |
visual question answering | |
Visualisation | |
Visualization | |
vote | |
VSCode | |
W | |
Warded Datalog+/- | |
weakening | |
weakenings of transitivity | |
Weakest pre-expectations | |
web | |
Web application | |
Web Playground | |
WebAssembly | |
website authentication | |
Weight learning | |
Weighted automata | |
weighted constraint satisfaction problem | |
Weighted First Order Model Counting | |
Weighted Max#SAT | |
weighted maximum satisfiability | |
weighted model counting | |
Weighted Projected Model Counting | |
Weisfeiler-Leman | |
Welcome | |
well-founded semantics | |
well-quasi-ordering | |
Well-quasiorders | |
while programs | |
whiteboard | |
Wittgenstein | |
Wordpress | |
Work-life Balance | |
workflow nets | |
workflow satisfiability problem | |
Workshop | |
X | |
XAI | |
XCSP3 | |
ximplified proofs | |
XML | |
XOR-CNF | |
Y | |
Yoneda lemma | |
Young Researcher | |
Z | |
ZDD | |
zero-knowledge proof | |
ZK protocols | |
zkSNARKs | |
ZX-calculus | |
Ł | |
Łós-Tarski Theorem | |
λ | |
λProlog | |
ω | |
ω-automata |