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