GLOBAL TALK KEYWORD INDEX
This page contains an index consisting of author-provided keywords.
2 | |
2-valued semantics for logic programs | |
3 | |
3-Variable Property | |
A | |
Abduction | |
abductive logic programming | |
Abductive Reasoning | |
abnormal behavior detection | |
ABox | |
absoluteness | |
Absorption | |
Abstract algebraic logic | |
abstract argumentation | |
abstract argumentation semantics | |
abstract datatypes | |
abstract diagnosis | |
abstract dialectical frameworks | |
abstract domain | |
abstract domain combinator | |
abstract domain of polyhedra | |
abstract DPLL | |
Abstract Elementary Classes | |
abstract interpretation | |
abstract machine | |
Abstract Machines | |
Abstract Model Theory | |
abstract state machine | |
Abstraction | |
Abstraction refinement | |
abstraction-refinement | |
ac0 | |
ACC | |
access control | |
accidental | |
Accountability | |
Accountable escrow | |
Accountable-escrowed encryption | |
accumulation | |
Ackermann's Function | |
ACL2 | |
ACL2(r) | |
ACT-R | |
action | |
action and change | |
Action histories | |
action languages | |
Action Models | |
Actor Prolog | |
Acyclic queries | |
acyclicity properties | |
Admissible computability | |
admissible rule | |
admissible rules | |
Admissible strategies | |
adversary models | |
adverse interactions | |
Aeronautics | |
affine arithmetic | |
affine group over the integers | |
Affine logic | |
Agda | |
Agent Architectures | |
agent programming | |
Aggregates | |
aggregation | |
aggregators in probabilistic models | |
AI | |
ALC | |
ALCH | |
ALCQIO | |
algebra | |
Algebra of maps | |
algebraic counterpart | |
algebraic data types | |
Algebraic effect | |
Algebraic effects | |
algebraic effects and handlers | |
Algebraic logic | |
Algebraic Message Model | |
algebraic program structures | |
Algebraic semantics | |
Algebraic specification | |
Algebraic structure | |
algebraic unification | |
Algebraizable logics | |
Algorithm | |
Algorithm Configuration | |
Algorithm Schedules | |
Algorithm Selection | |
Algorithm Visualization | |
Algorithmic randomness | |
algorithms | |
Algorithms Portfolio | |
aliasing | |
Allen algebra | |
alliances in graphs | |
alpha equality | |
alternating pushdown systems | |
alternating temporal logic | |
alternating Turing machine | |
amalgamation | |
amalgamation property | |
AMBA | |
amortised resource analysis | |
Amortized Complexity | |
ample generics | |
analysis | |
Analytical hierarchy | |
analyticity | |
Ancestral logic | |
Android | |
Android permissions | |
angry birds | |
annotated code | |
annotations | |
anomalous human activity | |
Anonymity Guarantees | |
Anonymous Communication Protocols | |
answer extraction | |
Answer Set Programming | |
Answer Set Programming (ASP) | |
answer set programming extensions | |
Answer Set Solving | |
answer-set programming | |
anytime algorithms | |
API Design | |
app | |
app functionality | |
application | |
applications | |
Applications of HOL4 | |
Applications of logic to combinatorics | |
applicative bisimulation | |
applied KR for design computing | |
Approximate inference | |
approximate program equivalence | |
Approximate Reachability | |
approximate reasoning | |
approximated answers | |
approximation | |
Approximation Fixpoint Theory | |
approximation spaces | |
Approximation theorem | |
Approximations | |
Apéry constant | |
arctangent | |
Argument | |
argument game | |
Argumentation | |
argumentation framework | |
Argumentation frameworks | |
argumentation semantics | |
Aristotle | |
arithmetic | |
Arithmetical complexity | |
Arithmetical hirarchy | |
Arithmetized Completeness Theorem | |
Array programs | |
Arrays | |
artifact-centric systems | |
Artificial Intelligence | |
Artin-Schreier extensions | |
ASP | |
ASP debugging | |
ASP Solver | |
Assertions | |
assumptions | |
assurance | |
assurance case | |
Assurance cases | |
Asymmetric unification | |
Asynchronous interaction | |
asynchronous systems | |
Asyncrhonous Interaction | |
ATL | |
ATL and ATL* | |
ATL+ | |
Atomic Decomposition | |
Atomic flows | |
atomic models | |
Atomicity | |
ATP | |
ATP competitions | |
ATP process | |
Attack trees | |
Attractor | |
attribute transition | |
attribute-based encryption | |
auction strategy | |
auction theory | |
Audit | |
authentication | |
autoepistemic logic | |
Automata | |
automata theory | |
Automata-Based Reasoning | |
automate reasoning | |
automated deduction | |
Automated design | |
automated planning | |
Automated Program Verifiers | |
automated reasoning | |
automated testing | |
automated theorem prover | |
automated theorem proving | |
automated theorem proving process | |
Automated theorem proving via SMT solver | |
automated verification | |
automatic annotation | |
automatic program calculation | |
automatic sequences | |
automatic structures | |
automatic theorem provers | |
Automatic verification | |
automation | |
Automation of Mathematics | |
automatizability | |
Autonomous systems | |
autonomy oriented computing | |
autostability | |
auxiliary relations | |
AVATAR | |
avoidability | |
awareness | |
axiom of determinacy | |
axiom of global choice | |
axiomatic logic | |
axiomatic semantics | |
Axiomatics | |
axiomatization | |
Axiomatization of Admissible Rules | |
Ayciclicity conditions | |
B | |
Bachmann's H(1) | |
back and forth | |
back-and-forth | |
backdoor set | |
backdoor sets | |
backdoors | |
background theories | |
Backtracking | |
Backtracking Algorithms | |
Backtracking Search | |
backward induction | |
backward proof search | |
Balanced tree data structures | |
Banach space | |
Banzhaf index | |
Bar recursion | |
bases for admissible rules | |
Batch verification | |
Bayesian inference | |
Bayesian model selection | |
Bayesian networks | |
BDD | |
Beagle | |
Beam Splitter | |
behavior of 2-formulas | |
Behavioral Synthesis | |
Behavioural Differential Equations | |
belief base | |
Belief bias | |
belief change | |
Belief Merging | |
belief probability | |
belief revision | |
Belnap-Dunn logic | |
benchmark | |
Benchmarking | |
benchmarks | |
benign | |
Bernays | |
Bernstein basis | |
Best Response Dynamics | |
Beth definability property | |
Betweenness centrality | |
BHK | |
BHK interpretation | |
Bi-Abduction | |
bi-immunity | |
bi-intuitionistic logic | |
biaffine PROP | |
Bialethism | |
Bidirectional | |
BiFL-algebras | |
Big Data | |
Bilinear Pairing | |
bimodule | |
binary decision diagram | |
binary decision diagrams | |
binders | |
biocompilaton | |
Bioengineering | |
Biological Networks | |
biological systems | |
biology | |
BioPortal | |
bipolar argumentation | |
birth/death and marriage records | |
bisimulation | |
bisimulation invariance | |
Bisimulation Quantifiers | |
bisimulation up-to | |
bit-vector | |
Bit-vector Preprocessing | |
bit-vectors | |
Bitopological Semantics | |
BL | |
blind multi-counter automata | |
block-ciphers | |
Blocked Clause Decomposition | |
Blocked Sets | |
blog | |
Blum-Shub-Smale | |
bmc | |
Boehm tree | |
Boolean algebra | |
Boolean Algebra and Presburger Arithmetic | |
Boolean Cardinality | |
Boolean circuit complexity | |
Boolean games | |
Boolean optimization | |
boolean-valued model | |
boosting completeness | |
Bootstrapping | |
Borel determinancy | |
Borel flows | |
Borel measurable payoffs | |
bottom-up evaluation | |
Bound Analysis | |
bounded arithmetic | |
bounded model checking | |
bounded morphisms | |
Bounded Polymorphism | |
bounded quantifier alternation | |
bounded treewidth | |
bounded ultrapower | |
Boundedness problem | |
Bounds-propagation | |
BPMN | |
Branching Time | |
branching VASS | |
BreakIDGlucose | |
Brownian motion | |
Brzozowski derivatives | |
Buchholz rule | |
Buchi automata | |
bulk synchronous parallelism | |
Business Process Management | |
Byzantine Failures | |
Büchi automata | |
C | |
C verification | |
C. I. Lewis | |
CafeOBJ | |
Calculus of Inductive Constructions | |
Calculus of structures | |
Call by name | |
Call by value | |
call-by-name | |
call-by-name and call-by-value | |
call-by-need lambda calculus | |
call-by-value | |
canonical formulas | |
Canonical structures | |
canonicity | |
Cantor | |
Cantor's Diagonal Argument | |
Cantor's Theorem | |
Cantor-Bendixson rank | |
capabilities | |
cardinal invariants | |
cardinal number | |
cardinality | |
cardinality constraints | |
Careflow | |
case studies | |
Categorical semantics | |
categoricity | |
category theory | |
Caucal hierarchy | |
causal graph | |
Causality | |
Causality in Databases | |
causation | |
cautious reasoning | |
CCS | |
CDCL | |
CDCL algorithm | |
CDCL solvers | |
cdf interval | |
ce degrees | |
CEGAR | |
CEGIS | |
cellular automaton | |
Central Limit Theorem | |
CERES | |
certain answers | |
certain knowledge | |
Certificates | |
certification | |
Certifying Algorithms | |
Certifying transformation | |
chaining predictors | |
challenging | |
Change Management | |
channel capacity | |
chaos theory | |
Chaotic Liar | |
characterisation theorem | |
characteristic formulae | |
Characterizing Cardinals | |
chemical master equation | |
Chemical Reaction Network | |
Chemical reaction networks | |
Chinese Remainder Theorem | |
chromatic number | |
Church Rule | |
Church's type theory | |
Church-Fitch | |
Church-Henkin type theory | |
Church-Rosser | |
Cichoń's diagram | |
CIG Acquisition | |
circuit complexity | |
circuit lower bounds | |
circuits | |
circular proofs | |
circularly ordered structure | |
circumscription | |
claim | |
class of structures | |
classes | |
classical first-order logic | |
classical first-order logic with inductive predicates | |
classical linear logic | |
classical logic | |
Classical Modal Logics | |
Classical Planning | |
Classical Propositional Logic | |
Classical realizability | |
Classification | |
classification theory | |
clausal proofs | |
Clause Learning | |
clause sharing | |
clinical decision support | |
clinical decision support systems | |
clinical education | |
Clinical Guidelines | |
clinical practice guideline | |
clinical practice guidelines | |
clinical processes | |
Clinical Trial Protocols | |
Clique-Width | |
clitic pronouns | |
clones with constants | |
Closed Sets | |
cloud computing | |
CLP applications | |
Clustering | |
CNF formulas | |
CNF partitioning | |
co-analytic sets | |
Co-NP completeness | |
coalgebra | |
coalgebras | |
Cobham recursion | |
Cobham recursive set functions | |
codata | |
codatatypes | |
code generation | |
code verification | |
coding | |
Coercion | |
coercions | |
Cognitive Modeling | |
cognitive robotics | |
Cognitive Science | |
Cognitive Semantics | |
coherence | |
Coherent Light | |
coinduction | |
coinductive predicates | |
Coinductive Types | |
Collaboration | |
Collapsible Pushdown Systems | |
collection scheme | |
collective coin flipping | |
Coloring number | |
Combination | |
Combination method | |
combination of equational theories | |
Combination problem | |
Combinatorial hypermap library | |
Combinatorial optimization | |
combinatorial proof | |
Combinatorial proofs | |
combinatorial topology | |
combinatorics | |
Combined Approach | |
combined complexity | |
Common Logic | |
Commonsense reasoning | |
communicating automata | |
communicating finite-state machines | |
Community detection | |
Community Structure | |
commutative context-free grammars | |
Comorbidity | |
Compact Closed Categories | |
compactness | |
Comparative evaluations | |
Comparative user evaluation | |
comparatives | |
compartmental models | |
competency question | |
competitive events | |
Compilation | |
Compiler certification | |
compiler construction | |
compiler intermediate representation | |
compiler verification | |
Complete lattices | |
complete partial orders | |
complete semilattice | |
completely order reflecting | |
completeness | |
completeness for isomorphisms | |
completeness of first-order logic | |
completeness theorem | |
Completeness theorem for classical logic | |
Completeness theorems | |
completion | |
completions | |
complex events | |
complex events recognition | |
complex networks | |
complexity | |
complexity analysis | |
complexity hierarchies | |
complexity of evaluation | |
complexity of query answering | |
complexity of rewriting | |
complexity theory | |
complexity-theoretic hierarchies | |
Composition Lemma | |
Composition Synthesis | |
Compositional Semantics | |
compositionality | |
comprehension model | |
compressed words | |
compression | |
computability | |
Computability and complexity | |
computability theory | |
computable analysis | |
computable categoricity | |
computable dimension | |
computable functions | |
Computable linear order | |
Computable linear orderings | |
computable model theory | |
Computable numbering | |
computable numberings | |
computable structure | |
computable structure theory | |
computably enumerable equivalence relations | |
computably enumerable graphs | |
Computation of least general generalizations for nominal terms | |
computational cognitive modeling | |
Computational Complexity | |
computational content | |
computational indistinguishability | |
computational linguistics | |
computational logic | |
computational model of narrative | |
Computational Models | |
Computational models of argument | |
computational neuroscience | |
Computational Pragmatics | |
computational psychology | |
computational reflection | |
computational semantics | |
computational social choice | |
computational soundness | |
computer algebra | |
computer interpretable guideline (CIG) | |
computer music | |
Computer Science Education | |
computer vision | |
computer-aided architecture design | |
Computer-Aided Cryptography | |
computer-interpretable guidelines | |
computer-supported collaborative work | |
Concept Learning | |
Concept matching | |
Concept Similarity | |
conceptual model | |
Conceptual Similarity | |
Concolic | |
Concolic Testing | |
concrete domains | |
concurrency | |
concurrency and synchronization | |
Concurrency Testing | |
concurrent constraint paradigm | |
Concurrent Constraint Programming | |
Concurrent Data Structures | |
Concurrent datatypes | |
Concurrent functional programming | |
Concurrent interaction net reduction | |
concurrent logic programming | |
Concurrent Programming | |
Concurrent programs | |
Concurrent stack | |
Concurrent systems | |
Condensed-matter physics | |
condition elimination | |
conditional logic | |
conditional logics | |
Conditional Queries | |
conditional rewriting | |
Conditional Term Rewriting | |
conditional term rewriting system | |
conference management system | |
confidentiality | |
conflict resolution | |
confluence | |
confluence in algebra | |
Conformance analysis | |
conformant planning | |
ConGolog | |
congruence | |
Congruence Closure | |
Congruential logics | |
conjunctive queries | |
Conjunctive query answering | |
conjunctive query evaluation | |
Connectedness | |
connection calculus | |
connection matrices | |
consensus | |
Consequence relation | |
Consequence-based Calculus | |
consequence-based reasoning | |
Consequences | |
conservative extension | |
Conservative extensions to stable model semantics | |
conservativity | |
Consistency | |
Consistency Checking | |
Consistent query answering | |
Constant Definition | |
constrained clauses | |
constrained ordered resolution | |
Constraint ASP | |
Constraint Handling Rules | |
Constraint Horn Clause | |
constraint logic | |
Constraint Logic Program | |
Constraint Logic Programming | |
Constraint Postponement | |
constraint programming | |
Constraint Propagation | |
constraint reasoning | |
constraint satisfaction | |
constraint satisfaction problem | |
Constraint satisfaction problems | |
constraint solver | |
constraint solving | |
Constraint-based synthesis | |
Constraints | |
constraints-based | |
construction | |
constructive algebra | |
Constructive logic | |
constructive mathematics | |
constructive negation | |
constructive reverse mathematics | |
Constructive temporal logic | |
Constructive type theory | |
Content representation | |
context | |
context free grammars | |
context schemas | |
context semantics | |
Context-based Reasoning | |
context-free grammars | |
context-free sets of graphs | |
context-sensitive rewriting | |
Contexts | |
contextual equivalence | |
Contextual Reasoning | |
contextualized description logics | |
contingent planning | |
continuation | |
continuation passing Prolog | |
continuation semantics | |
continuations | |
continuous noise in effectors and sensors | |
continuous payoffs | |
Continuous Time | |
continuous time Markov chains | |
contraction | |
contracts | |
contradiction | |
Contradictions | |
Control | |
Control Flow Analysis | |
Controllability | |
controller | |
controller synthesis | |
Conversion | |
conversion algorithm | |
conversion equivalence | |
Conversions | |
convex hull | |
convex optimisation | |
convex structures | |
Coordination Games | |
copattern matching | |
COPD | |
Coq | |
Coq 8.5 | |
Coq proof assistant | |
Coq/SSReflect | |
Coq/SSReflect Proof Assistant | |
Corecursion | |
cores | |
correct program transformation | |
correctness | |
correctness criterion | |
Correctness Proofs | |
cost automata | |
Cost Models | |
cost monadic second-order logic | |
countable choice | |
Countably categorical structures | |
Counterexamples | |
countermeasures | |
counting | |
counting functions | |
counting quantifiers | |
Coupling | |
Courcelle's theorem | |
coverability problem | |
coverage metrics | |
CP | |
CP-logic | |
CP-nets | |
CPA | |
cps translation | |
CPS-translation | |
Craig interpolation | |
Craig's interpolation | |
crash-tolerant | |
crawling | |
creative telescoping | |
Criterion~H | |
critical pair | |
critical pairs | |
critical peak | |
critically trivial | |
cross-sections of flows | |
crowd sourcing | |
cryptographic definitions | |
Cryptographic protocol analysis | |
cryptographic protocols | |
Cryptoki | |
CSP | |
CTL | |
cumulative quantification | |
Cumulativity | |
cut elimination | |
cut-elimination | |
cut-introduction | |
cutoff | |
cutoffs | |
Cutting and Packing | |
cyber-insurance | |
cyber-physical security protocols | |
cyber-physical systems | |
Cycle rewriting | |
cyclic and structural induction | |
cyclic lambda-terms | |
D | |
Dalvik | |
Danos-Regnier criterion | |
data complexity | |
data mining ontology | |
data structures | |
data structures for tableaux calculi | |
data synchronization | |
data trees | |
data visualization | |
Data-aware dynamic systems | |
database | |
Database generation | |
database querying | |
Database semantics | |
database theory | |
Databases | |
Databases Repair | |
Datalog | |
Datalog rewritability | |
datalog rewriting | |
Datapath Abstraction | |
datasets | |
Datatypes | |
datatypes à la carte | |
Davies-trees | |
De Bruijn | |
de Bruijn indices | |
de Morgan algebras | |
de Morgan logic | |
de Morgan negation | |
deadlock | |
Debugging | |
decidability | |
decidability and complexity | |
Decidability results | |
Decision | |
decision diagrams | |
decision method | |
decision problems | |
decision procedure | |
decision procedures | |
decision rules | |
Decision trees | |
declarative modeling | |
declarative programming | |
declarative programming language constructs | |
declarative specification | |
Declarative systems | |
declassification | |
decomposition | |
decomposition theorems | |
decreasing diagrams | |
deduction | |
deduction modulo | |
deductive compilation | |
deductive databases | |
deductive program verification | |
deductive verification | |
deep | |
Deep inference | |
Deep relevant logics | |
default logic | |
default negation | |
default reasoning | |
defeasible inheritance | |
defeasible knowledge | |
defeasible logic program | |
defeasible reasoning | |
Defectivity | |
definability | |
definability of truth | |
definable groups | |
Definable well-orders | |
Definition evaluation | |
Definition refining | |
definitional package | |
degree | |
degree of autostability | |
degree sequences | |
Degree spectra | |
degree spectra of relations | |
degree spectrum | |
degree structure | |
degree theory | |
degrees of belief | |
degrees of truth | |
delay | |
delegatable anonymous credentials | |
delimited control operators | |
Delineation semantics | |
demonstration | |
Denjoy integration | |
denotational semantics | |
Densification | |
density elimination | |
deontic logic | |
dependence | |
dependence logic | |
dependencies | |
Dependency graphs | |
dependency pair framework | |
dependency parsers | |
Dependency Schemes | |
dependent elimination | |
dependent type theory | |
dependent types | |
dependently typed lambda calculus | |
dependently typed languaged | |
Dependently-typed programming | |
Depth relevance | |
derivability | |
Derivational complexity | |
Description logic | |
Description Logic Ontologies | |
Description Logics | |
Description Logics and Ontologies | |
descriptive complexity | |
Descriptive complexity theory | |
Descriptive set theory | |
Design | |
determinacy | |
deterministic transitive closure | |
determinization | |
Device Drivers | |
Device Enrolment | |
diagnosis | |
diagnosis discrimination | |
Diagnosis of Arterial Hypertension causes | |
Diagnostic Reasoning | |
Diagonalization | |
diagonally non-computable | |
diagrams | |
Dialectic Logic | |
Dialectica translation | |
dialog systems | |
Dialogical argumentation | |
dialogical logic | |
Dialogical Proof Theory | |
dialogical semantics | |
dialogue | |
dialogue games | |
Dialogue Modeling | |
dict | |
Difference Equations | |
Difference hierarchy | |
differentiability | |
Differential Evolution | |
Differential fields | |
Differential Linear Logic | |
differential power analysis | |
Differential Privacy | |
Differential Temporal Dynamic Logic | |
Differentiation | |
Diffie-Hellman | |
Diffie-Hellman key exchange | |
Diffnets | |
Diffusion Dynamics | |
digital forensics | |
digital repository | |
digital revolution | |
dilation | |
Direct style | |
Directed Testing | |
discourse analysis | |
Discrete dynamical systems | |
Discrete Time Markov Chain | |
discrimination tree | |
disjoint amalgamation | |
disjoint unions | |
Disjunction Property | |
disjunctive answer set programming | |
Disjunctive Datalog | |
Disjunctive existential rules | |
disjunctive logic program | |
dispensability | |
display calculi | |
display type calculus | |
distance metrics | |
Distributed Algorithm | |
distributed algorithms | |
distributed computing | |
Distributed Constraint Optimization Problems | |
distributed hybrid systems | |
distributed programming | |
distributed search | |
distributed system | |
Distributed Systems | |
distributed version control systems | |
Distributed-Algorithms | |
Distribution Semantics | |
Distributional Semantics | |
distributive lattice | |
distributivity | |
Diversification | |
divide-and-conquer | |
DL Lite | |
DL reasoning | |
DL-Lite | |
DL-programs | |
DL-safe rules | |
DNA computing | |
DNA nanotechnology | |
DNA Strand Displacement | |
DNC | |
DNF duality | |
DNF minimization | |
documentation | |
domain | |
Domain Independence | |
domain specific modeling | |
domain theory | |
Domain-specific languages | |
domains | |
Dominance | |
Dominating Functions | |
domination | |
Double negation shift | |
Double negation translation | |
downward closure | |
doxastic logic | |
DPLL | |
DPLL(T) | |
DQBF | |
DQBF solving | |
DQDIMACS | |
DRed | |
DRUP | |
duality | |
Dynamic Algebra | |
Dynamic Analysis | |
dynamic complexity | |
dynamic consistency checking | |
dynamic contexts | |
Dynamic Domains | |
Dynamic Epistemic Logic | |
dynamic games | |
Dynamic information flow control | |
dynamic logic | |
dynamic logics | |
dynamic pattern calculus | |
Dynamic Predicate Logic | |
dynamic programming | |
dynamic quantification | |
Dynamic reasoning | |
dynamic security enforcement mechanisms | |
Dynamic systems | |
dynamic techniques | |
dynamical model | |
dynamical systems | |
E | |
e-Health | |
E-matching | |
Eager Languages | |
Earley deduction | |
Eclipse | |
economics | |
economics of security | |
editing | |
education | |
EF Games | |
effect handling | |
effect system | |
effective bi-immunity | |
effective bounds | |
effective computation | |
effective reducibility | |
effectivity properties | |
Efficient protocols | |
efficient refinement check in VCC | |
EFL-ontology | |
egalitarianism | |
Ehrenfeucht-Fraisse games | |
Ehrenfeucht-Fraïssé games | |
EL | |
EL TBoxes | |
Elections | |
elementary algorithms | |
elementary epimorphism | |
elementary equivalence | |
elementary indivisibility | |
elementary interpretations | |
elementary submodels | |
Elliptic Curves | |
embedded systems | |
embedding | |
Emil Post | |
Empire | |
empirical analysis | |
Empirical investigation | |
Emptiness | |
Emptiness Check for Generalized Buchi Automata | |
end-extensions | |
endocytosis | |
Energy games | |
Engineering | |
Entropy of formal languages | |
enumeration | |
enumeration degrees | |
enumeration of family | |
enumeration operator | |
enumeration reducibility | |
enumerators | |
environment assumptions | |
epidemic models | |
epistemic entrenchment | |
epistemic logic | |
epistemic logic programs | |
epistemic planning | |
Epistemic reasoning | |
Epistemic Specification | |
epistemic specifications | |
epistemic temporal specification | |
EPR | |
Epsilon | |
epsilon-recursion | |
Equality | |
Equality constraints | |
equational base | |
equational constraint | |
equational logic | |
equational simplification | |
equational translation | |
Equational Unification | |
equationally definable | |
Equationally orderable quasivarieties | |
equations over types | |
equilibrium logic | |
Equilibrium Semantics | |
equivalence | |
equivalence properties | |
equivalence relation | |
Equivalence relations | |
equivariance | |
Error Explanation | |
Error localization | |
Error-correcting codes | |
Error-tolerant reasoning | |
Ershov hierarchy | |
Escrowed public key | |
ESL Design | |
esoteric language | |
Euclid's Theorem | |
evaluation | |
evaluation of clinical guideline models | |
Event structures | |
Event-B | |
events API | |
evidence | |
exact algebra | |
Exact Inference | |
Exact Learning | |
exact real-number computation | |
excellence | |
Excessiveness | |
Executable Formal Models | |
execution | |
execution monitoring | |
Execution monitors | |
Existence | |
Existence Property | |
existential interpretation | |
existential rules | |
existentially closed model | |
Expected mean-payoff | |
Experiment | |
experiment design | |
Experimental Evaluation | |
Experimental mathematics | |
Experimentations | |
Experiments | |
Explanations | |
Explicit Mathematics | |
Explicit Substitutions | |
explosion rule | |
explosiveness | |
exponential integer part | |
exponential modality | |
exponential time algorithm | |
exponentiation | |
expressive completeness | |
Expressive Description Logics | |
Expressive Ontologies | |
expressive power | |
expressive TBoxes | |
expressiveness | |
EXPSPACE | |
Extended Church Principle ECT and the Uniformization Principle UP | |
Extended resolution | |
extensional model | |
extensional models | |
extensionality axiom | |
extensions of models | |
External Numbers | |
Extraction | |
Extreme amenability | |
F | |
Faceted search | |
FaCT++ | |
failed literal detection | |
Failure Resilience | |
Failures of the GCH | |
Fair CTL | |
Fair Termination | |
fairness | |
Fan Functional | |
fast-growing complexity | |
Fault Localization | |
fault-tolerance | |
fault-tolerant computing | |
feasibility checks | |
feasible set functions | |
feature extraction | |
feeble orthogonality | |
Feferman-Vaught | |
fibrations | |
Fiduccia-Mattheyses algorithm | |
field theory | |
Fields | |
filter-model | |
filtrality | |
Finitary matching | |
Finite and Infinite Transition Systems | |
finite automata | |
finite domain | |
Finite Domain Solver | |
finite inseparability | |
Finite Lattices | |
finite mixtures | |
Finite model property | |
Finite model theory | |
finite satisfiability | |
Finite satisfiability and implication algorithm | |
finite variable fragments | |
Finite-valued Logic | |
Finiteness | |
Firewall | |
First order | |
first order logic | |
first order logic with majority quantifiers | |
First Order Monadic Logic | |
First-Degree Entailment | |
first-order | |
First-order classical proof nets | |
First-order Classical Sequent Calculus | |
first-order intermediate language | |
first-order logic | |
First-Order Logic Model Checking | |
first-order logic of discrete linear order | |
first-order modal logic | |
First-order modal logics | |
first-order model checking | |
first-order predicate fuzzy logics | |
First-order temporal logic | |
first-order term rewriting | |
first-order theorem proving | |
Fisher information matrix | |
five-valued LTL | |
fix-sized subontologies | |
fixed parameter tractability | |
fixed parameter tractable | |
fixed point operators | |
Fixed point theory | |
fixed-parameter complexity | |
fixed-parameter tractability | |
Fixed-parameter tractable algorithms | |
Fixed-Points | |
Fixpoint Logic | |
Fixpoints | |
FL-algebras | |
FL_0 | |
Flattening | |
FLew-algebra | |
floating point | |
Floating-label systems | |
Floating-point arithmetic | |
floor function | |
Flow-sensitive references | |
flow-table | |
Floyd-Hoare logic | |
FLP | |
flux balance analysis | |
fMV-algebra | |
FO(.) | |
focalisation | |
Focus Groups | |
focused derivations | |
Focusing | |
focusing proofs | |
fodot | |
forcing | |
Forcing axioms | |
Forgetting | |
Forgetting in Reasoning about Actions | |
Forgetting in the Situation Calculus | |
Forgetting/projection/uniform interpolation | |
Forking | |
formal fuzzy logic | |
formal mathematics | |
Formal Metatheory | |
formal methods | |
formal model | |
Formal models | |
Formal semantics | |
formal specification | |
Formal verification | |
formal verification of OS | |
Formalisation | |
formalisation of clinical guidelines | |
formalisms | |
formalization | |
Formalization of Language Semantics | |
Formalization of mathematics | |
formalization of medical processes and knowledge-based health-care models | |
formalized mathematics | |
ForMaRE | |
Formats | |
Forms of agitation | |
formula | |
formula trimming | |
formulae-as-types | |
formulas with two occurrences | |
forward induction | |
forwarding rule | |
foundations | |
Foundations of Logic | |
Foundations of Mathematics | |
Fractal Dimension | |
fractals | |
Fragments of arithmetic | |
fragments of MA | |
Fragments of Propositional Logic | |
Fraisse limits | |
framework | |
Framing | |
Frege | |
Frege proofs | |
Frege systems | |
full abstraction | |
full intuitionistic linear logic | |
Full trees | |
fully invertible and injective programs | |
fun | |
Function combinators | |
function fields | |
function introduction | |
functional dependencies | |
Functional instantiation | |
functional notation | |
functional programming | |
Functional reactive programming | |
functional roles | |
functor | |
Fundamental Sequences | |
fuzzy | |
Fuzzy Description Logic | |
Fuzzy Description Logics | |
fuzzy likelihood | |
fuzzy logic | |
Fuzzy logic for medical knowledge | |
fuzzy logics | |
Fuzzy modal logic | |
Fuzzy Ontologies | |
fuzzy plurivaluationism | |
fuzzy probability | |
fuzzy quantification | |
fuzzy usuality | |
G | |
gain function | |
Gale-Stewart games | |
Gallina | |
Galois theory | |
Galoius Types | |
game characterisations | |
Game Semantics | |
game theories | |
Game theory | |
game-theoretical semantics | |
Games | |
games in logic | |
Games on graphs | |
Games on Networks | |
gamification | |
Gappiness | |
Gathering | |
gene expression | |
gene regulatory network | |
General logic | |
General Models | |
general relativity | |
General resolution | |
General safe recursion | |
general stable models | |
general theory of stable models | |
generalised entropy measurements | |
Generalization of nominal terms-in-context | |
generalized computability | |
Generalized Craig interpolation | |
Generalized databases | |
Generalized Hypertree Decomposition | |
generalized predicativity | |
Generalized Quantifiers | |
generalized rational grading | |
generalized truth value | |
generating functions | |
generic | |
generic extensions | |
generic programming | |
genericity | |
Genetic algorithms | |
genetic gates | |
Gentzen | |
Gentzen's sharpened Hauptsatz | |
geometric | |
geometric logic | |
geometry | |
Geometry of Interaction | |
germinal ideal | |
ghost code | |
git | |
GLEE | |
GLIF | |
Glivenko's theorem | |
Glivenko’s theorem | |
global assumptions | |
global caching | |
Global Constraints | |
Global Optimisation | |
global sensitivity analysis | |
Glucose | |
goal-directed | |
Godel logic | |
Godel negative translation | |
Goedel T-norm | |
Golog | |
GPGPU programming | |
GPGPUs | |
GPU | |
GPUs | |
GR(1) synthesis | |
graded modal logic | |
Graded theories | |
grammars | |
graph algorithms | |
Graph calculi | |
graph decomposition | |
graph property | |
graph rewriting | |
Graph structured data | |
graph theory | |
graph-based formulas | |
graphical specification patterns | |
Graphical user interface | |
graphics processing units | |
Graphs | |
Ground Tree Rewrite Systems | |
Grounded Equilibrium Semantics | |
grounded Martin's axiom | |
Grounding | |
Grounding bottleneck | |
GSOS | |
Guarded fragment | |
guarded logics | |
Guarded recursion | |
Guardedness | |
Guards | |
Guideline representation | |
guideline transformation | |
Guillotine Constraint | |
Gödel 3-valued logic | |
Gödel logics | |
Gödel Semantics | |
Gödel t-norm | |
Gödel's incompleteness theorem | |
H | |
Hallden completeness | |
Hamiltonian Cycle Problem | |
Hanf-locality | |
hard constraint | |
hard SAT instances | |
hard subsets | |
hardness | |
hardness results | |
hardware | |
Hardware design | |
hardware verification | |
Hash Tries | |
hashing | |
Haskell | |
HCV | |
Health Care | |
health histories | |
healthcare | |
heap structures | |
Henkin Quantifier | |
Henkin's proof | |
Herbrand functions | |
Herbrand model | |
Herbrand Sequent | |
Herbrand theorem | |
Herbrand's theorem | |
Hereditarily finite superstructure | |
HermiT | |
Heuristics | |
Heyting algebra | |
Heyting Algebra Expansions | |
Heyting Arithmetic | |
Heyting's logic | |
hidden features | |
hierarchical planning | |
Hierarchized linked implementation | |
hierarchy of norms | |
high assurance | |
High Level Synthesis | |
High School Timetabling | |
high-performance computing | |
Higher dimensional structures | |
Higher Order Logic | |
Higher Order Program Analysis | |
higher-dimensional rewriting | |
higher-order | |
Higher-order automated theorem provers | |
Higher-order description logics | |
higher-order logic | |
higher-order logic programming | |
higher-order model checking | |
higher-order model-checking | |
Higher-order pattern unification | |
higher-order pi-calculus | |
Higher-order programs | |
higher-order recursion schemes | |
higher-order rewrite systems | |
higher-order term graphs | |
higher-order term rewriting | |
higher-order unification | |
hilbert | |
Hilbert axiomatisation | |
Hilbert axiomatizations | |
Hilbert Axioms | |
Hilbert systems | |
Hilbert's Tenth Problem | |
History of Logic | |
HIV | |
Hoare assertions | |
Hoare logic | |
Hoare's logic | |
HOAS | |
HOL | |
HOL Light | |
HOL4 | |
HOL4 for non-computer science community | |
homogeneous frames | |
homogeneous models | (LC) |
homogeneous structures | |
Homological algebra | |
homomorphism preservation in the finite | |
homomorphisms | |
homotopy | |
homotopy type theory | |
honest elementary degrees | |
hoops | |
horn | |
Horn logic | |
Horn theories | |
HPC | |
Hrushovski construction | |
HS-posets | |
html | |
Human Behavior | |
Human Factors | |
Human Reasoning | |
Human-computer interaction | |
hybrid algorithm | |
hybrid automata | |
Hybrid Logic | |
Hybrid Logics | |
hybrid spatial-nonspatial simulations | |
hybrid stochastic simulation | |
hybrid stochastic simulations | |
hybrid stochastic-deterministic simulations | |
hybrid system modelling | |
hybrid system models | |
hybrid systems | |
Hyper-Ackermannian complexity | |
hyperarithmetic hierarchy | |
hyperarithmetical hierarchy | |
hypergraph | |
Hypergraph decomposition | |
hypergraph duality | |
hypergraph partitioning | |
Hypergraph transversals | |
Hypergraphs | |
Hypersequent Calculi | |
hypersequents | |
Hyprgraphs | |
I | |
ic3 | |
IC3/PDR | |
IDE | |
Ideal | |
ideals | |
Idempotent Semiring | |
identification constraints | |
Identification of proofs | |
identity | |
IDP | |
IDP3 | |
IEEE standard | |
IF logic | |
Immunization strategy | |
Imperative Program | |
imperfect information | |
Implementation | |
Implementation and Optimisation Techniques | |
Implementation of dialogical argumentation | |
Implementation Techniques | |
implicant minimization | |
implication fragments of substructural logics | |
implicative fragment | |
Implicature | |
implicit commitment | |
Implicit Complexity | |
implicit computational complexity | |
Implicit Definition | |
implicit generalization | |
implicitly definable | |
important separators | |
improvements in theorem prover technology | |
incomplete databases | |
incomplete information | |
Incompleteness | |
inconsistency | |
inconsistency handling | |
inconsistency in probabilistic knowledge bases | |
inconsistency measures | |
inconsistency-tolerant query answering | |
incremental evaluation | |
Incremental Preprocessing | |
Incremental reasoning | |
Incremental SAT | |
Incremental SAT Solving | |
incremental tabling | |
incremental verification | |
independence | |
indexing | |
IndiGolog | |
indiscernibility | |
indiscernible | |
Indiscernibles | |
Individual concepts | |
Indivisibility | |
Induction | |
induction reasoning | |
induction rule | |
Induction schemes | |
Inductive definition | |
inductive definitions | |
inductive invariant | |
inductive predicates | |
Inductive Reasoning | |
inductive synthesis | |
Industrial automation | |
inference | |
inference search | |
inferences | |
Infiniband | |
Infinitary Formulas | |
infinitary lambda-calculus | |
Infinitary Logic | |
infinitary proof theory | |
infinitary rewriting | |
Infinitary Trees | |
Infinite connected graph of bounded degree | |
Infinite execution | |
Infinite graph rewriting | |
infinite resumptions | |
Infinite tree | |
infinite-valued logics | |
infinitely | |
infix probability | |
Informal semantics | |
information economy principle | |
information flow | |
information flow control | |
Information Flow Security | |
Information Hiding | |
Information preservation | |
information retrieval | |
information system | |
Information theory | |
information-flow security | |
Inhabitation | |
initial algebra | |
inner models | |
Innocent strategies | |
Input Vectors | |
Input/output logic | |
insertion modeling | |
insider threat | |
Insider Threats | |
Inspection Points | |
instability | |
Instance features | |
Instance Queries | |
instance reducibility | |
instance-based theorem proving | |
instantiation | |
Instrospection | |
Int construction | |
integer part | |
integer programming | |
integers | |
Integrating CDCL and MP | |
Integration | |
integrity of OS | |
intelligent visual surveillance | |
intensional Martin-Löf type theory | |
Intensional transitive verbs | |
Intensionalization | |
Intention and Belief | |
intentional semantics | |
interacting particle systems | |
Interaction | |
Interaction nets | |
interactive case simulation tools | |
interactive systems | |
Interactive Theorem Provers | |
interactive theorem proving | |
interactive verification | |
Interference Scenarios | |
intermediate | |
Intermediate Logics | |
intermediate models | |
Intermediate Predicate logics | |
intermediate verification language | |
internalization of type classes | |
interpolants | |
Interpolation | |
interpolation property | (LC) |
intersection | |
Intersection and union types | |
intersection type | |
intersection types | |
Interval analysis | |
interval arithmetic | |
Interval solvers | |
intervals | |
intrinsic variety | |
introspection | |
introspective reasoning | |
Intuitionism | |
intuitionistic | |
intuitionistic first-order theories | |
intuitionistic hybrid logic | |
intuitionistic logic | |
intuitionistic modal logic | |
intuitionistic propositional logic | |
intuitionistic set theory | |
intuitionistic-modal Kripke frames | |
invariance proofs | |
invariant computation | |
invariant synthesis | |
Invariants | |
inverse limit | |
inverse properties | |
inverse rewriting | |
inverse roles | |
Invited talk | |
involutive residuated lattice | |
IPC API | |
irrationality proof | |
Irregularity | |
Isabelle | |
Isabelle proof assistant | |
Isabelle/HOL | |
Isabelle/PIDE and Isabelle/jEdit | |
isar | |
Ising Model | |
isomorphism problem | |
IT support | |
iteration | |
iterative process | |
J | |
Janin-Walukiewicz theorem | |
Java | |
Java Virtual Machine (JVM) | |
JavaCard API | |
JavaScript | |
jEdit | |
Jeffrey's rule of conditioning | |
Jonsson theories | |
JSON Schema | |
Judgment Aggregation | |
jump | |
jump inversion | |
Just-in-time Compilation | |
justification | |
Justification Logic | |
Justifications | |
justified belief | |
K | |
k-fold Tseitin formula | |
k-liveness | |
k-SAT | |
Kachinuki ordering | |
Kechris-Woodin rank | |
kernel verification | |
key | |
Key Compromise Impersonation | |
KLEE | |
Kleene algebra | |
Kleene algebra with tests | |
Kleene logic | |
Klein four group | |
Knowability Paradox | |
Knowledge | |
Knowledge Acquisition and Forgetting | |
knowledge base | |
knowledge base revision | |
knowledge base system | |
knowledge compilation | |
knowledge obfuscation | |
Knowledge Representation | |
Knowledge representation and ontologies for health-care processes | |
Knowledge Representation and Reasoning | |
Knowledge-based training | |
Knuth-Bendix completion | |
Kripke frames | |
kripke model | |
Kripke models | |
Kripke Platek set theory | |
Kripke semantics | |
Krohn-Rhodes Theory | |
Kruskal-Katona Theorem | |
L | |
labelled Markov Chains | |
labellings enumeration algorithm | |
Lagrange duality | |
lambda calculus | |
Lambda encodings | |
lambda expressions | |
lambda-calculus | |
lambda-mu calculus | |
Lambek grammars | |
language classes | |
Language Design | |
Language Interoperability | |
language of mathematics | |
Language Translator | |
Languages | |
Large cardinals | |
Large Neighbourhood Search | |
large theories | |
large-scale ontologies | |
large-theory automated reasoning | |
Lasserre | |
Latin square | |
lattice of truth values | |
Lawvere theories | |
Lazy Annotation | |
lazy data structures | |
Lazy Languages | |
lazy lists | |
learning | |
Learning preferences | |
Lebesgue orbit equivalence | |
left-c.e. real | |
leftmost outermost | |
Leibniz congruence | |
Leibniz hierarchy | |
Leibniz operator | |
length | |
lessons learned | |
lexicographic product | |
Lexicographic Ranking Function | |
LF | |
Liar | |
Liar Paradox | |
Librationism | |
lie groups | |
Lifted inference | |
Lifting | |
light logics | |
limit laws | |
limitative results | |
limitative theorems | |
limited nondeterminism | |
limited recursion | |
limitwise monotonic degree | |
Limitwise monotonic function | |
limitwise monotonic functions | |
limitwise monotonic reducibility | |
limitwise monotonic set | |
Lindon interpolation | |
linear | |
linear algebra | |
linear arithmetic | |
linear constraints | |
linear differential systems | |
Linear lasso program | |
linear logic | |
linear logic programming | |
linear pi-calculus | |
linear real problems | |
linear rewriting and generalized gröbner basis | |
linear spaces | |
Linear Temporal Logic | |
linear time complexity | |
linear transformation | |
Linear Types | |
linear-time temporal logic | |
Linearity | |
Linearizability | |
link formulas | |
Linked Data | |
Linking | |
LIO | |
Liquid types | |
list homomorphisms | |
List-chromatic number | |
Lists | |
livelock | |
Liveness | |
LLVM | |
local consistency | |
local finiteness | |
local optimum | |
Local reasoning | |
Local Search | |
Local state monad | |
local temporal logic | |
local theories | |
local theory extensions | |
local typedef | |
local-first | |
locality | |
locally finite variety | |
lock-free data structures | |
Lock-freedom | |
Logarithmic Space | |
logic | |
logic education | |
logic of common knowledge | |
logic of GK | |
logic of here-and-there | |
logic of infinite sequences | |
Logic of Paradox< |