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