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 | |
Logic of Proofs | |
Logic of Scientific Discovery | |
Logic over graphs | |
Logic Progarms | |
logic program updates | |
logic programming | |
Logic solvers | |
logic translation | |
logic variables | |
Logic-based Knowledge Representation | |
logic-based modeling | |
Logical abduction | |
logical analysis of algorithms | |
Logical annotations | |
Logical aspects of computational complexity | |
logical difference | |
Logical Errors | |
Logical Framework | |
Logical Frameworks | |
logical semantics | |
Logics | |
Logics for AI | |
logics for graphs | |
Logics for partial functions | |
Logistic Liar | |
logistic regression | |
Long-distance resolution | |
loop | |
Loop Analysis | |
Loop Detection | |
loop invariant | |
loop invariants | |
Loop Pipelining Transformation | |
Lorentzian manifolds | |
Los-Tarski | |
low and high degrees | |
low-level code | |
low-level programming languages | |
Lowenheim-Skolem theorems | |
lower bound | |
lower bounds | |
LP design and implementation | |
Ltac | |
LTL | |
LTL Model Checking | |
LTL Separation | |
LTL synthesis | |
Ludics | |
Lukasiewicz formulas | |
Lukasiewicz logic | |
Lyapunov exponents | |
M | |
m-Health | |
machine learning | |
Machine-Learning | |
Magic Sets | |
main-memory RDF store | |
majority operators | |
majority polymorphism | |
make-easy" teaching approach | |
malleable signatures | |
Many core | |
Many Valued Logics | |
many-valued | |
many-valued logic | |
Many-valued logics | |
Many-valued modal logic | |
Manycore | |
Mapping Analysis | |
mapping probabilistic logic languages | |
Mapping Visualization | |
MapReduce | |
MapReduce Framework | |
Maps of graphs | |
marked regular expressions | |
Marker's extensions | |
Markov Chain | |
Markov Chain Monte Carlo Techniques | |
Markov chains | |
Markov Principle M | |
Markov Rule | |
Markov's normal algorithms | |
Markov's Principle | |
Martin Lof randomness | |
Martin Lof test | |
Mass Parallelization | |
massive open online courses | |
Matching | |
matching logic | |
Matchmaking | |
Materialisation | |
Materialization | |
mathematical components | |
mathematical fuzzy logic | |
mathematical knowledge | |
mathematical logic | |
Mathematical Morphology | |
Mathematical progress | |
mathematics education | |
Mathias model | |
Matrix iterations | |
matrix multiplication | |
max-2-sat | |
Max-SMT | |
maximal completion | |
maximal contraction | |
Maximal Falsifiability | |
Maximal interpolants | |
Maximal Satisfiable Subsets | |
maximum entropy model | |
Maximum Falsifiability | |
Maximum Independent Set | |
Maximum satisfiability | |
Maximum satisfiability modulo theories | |
MaxSAT | |
MCMC | |
MDP | |
mean payoff | |
mean-payoff and discounted sum | |
mean-payoff games | |
meaning explanations | |
measurable cardinals | |
Measure | |
mechanism design | |
Mechanization of Mathematics | |
mechanized proof | |
Medical Knowledge Representation | |
medical treatment processes | |
MELL | |
memory fence synthesis | |
Memory Logics | |
Memory Safety | |
mereology | |
mereotopology | |
Message Formats | |
Message Passing | |
message passing systems | |
message sequence charts | |
Meta | |
Meta CIG system | |
meta modelling | |
meta programming | |
meta-heuristic search | |
meta-logic | |
metabolic regulation | |
metadata | |
metamathematics | |
metric abstract elementary classes | |
metric structures | |
metric temporal logic | |
micro-kernel OS | |
Midsequent theorem | |
MILS | |
MILS (multiple independent levels of security) | |
Min-closed constraints | |
MinAs | |
minimal change | |
Minimal Correction Subsets | |
minimal entailment | |
Minimal hitting set dualization | |
Minimal model generation | |
minimal model semantics | |
Minimal modules | |
minimal network | |
Minimal numbering | |
minimal numberings | |
minimal truth | |
Minimal Unsatisfiable Core | |
Minimal Unsatisfiable Subsets | |
Minimum Satisfiability | |
Minisat | |
Minkowski sum | |
Minlog | |
missing information | |
Mixin | |
mixin inheritance | |
MLL | |
MMT | |
MMU | |
Mnemoids | |
mobile computing | |
mobile devices | |
Mobile Robots | |
Modal and temporal logics | |
modal consequence operations | |
modal logic | |
Modal logics | |
Modal Logics of Confluence | |
modal mu-calculus | |
modal tableaux | |
Modal Temporal Logics | |
modal µ-calculus | |
Mode checking | |
model | |
model analysis | |
Model Checker | |
model checking | |
model composition | |
Model construction | |
model counting | |
model existence | |
model expansion | |
model finding | |
model generation | |
model revision | |
Model Synthesis | |
model theory | |
model theory of incompleteness | |
model validation | |
model-based reasoning | |
Model-Based System Development | |
model-based theorem proving | |
Model-checking | |
model-finding | |
modeling | |
modelling | |
modelling and analysis of qualitative behaviour of biological systems | |
models | |
models of incompleteness | |
modern proof theory | |
modes of operation | |
Modular Logic Programming | |
modular reasoning | |
Modular Solver | |
modular systems | |
modular verification | |
modulare SMT solving | |
Modularisation | |
modularity | |
modularization | |
Module systems | |
modules | |
modulo counting quantifiers | |
Molecular computing | |
Molecular programming | |
Monad | |
Monadic | |
monadic ASP | |
monadic language | |
monadic logic | |
Monadic metalanguages | |
monadic program schemes | |
monadic recursion schemes | |
monadic second order logic | |
monadic second-order | |
monadic second-order logic | |
Monads | |
Monads with arities | |
monitor | |
monitoring | |
Monoid | |
monomorphization | |
Monotone induction and coinduction | |
monotone modal logic | |
Monotone operator | |
Monotone proofs | |
monotonic abstraction | |
monotonic logic | |
Monotonic Markov decision processes | |
Montague semantics | |
Monte-Carlo Tree Search | |
Morley sequences | |
morphic words | |
MSO | |
MSO definable graphs of bounded clique-width | |
MSO-automata | |
MTL | |
mu-calculus | |
Muller games | |
multi agent | |
multi agent games | |
Multi Context Systems | |
multi type calculus | |
Multi-agent systems | |
Multi-Attribute Decision Making | |
multi-context system | |
multi-context systems | |
Multi-counter automata | |
Multi-Criteria Decision Making | |
Multi-Paradigm Programming | |
Multi-Stack Pushdown Systems | |
multi-type sequent calculi | |
Multi-valued logic | |
Multi-valued Logic Programming | |
multiagent dynamic systems | |
Multicore | |
Multicore shared-memory system | |
multidimensional quantitative games | |
multimedia learning modules | |
multiple-conclusion rule | |
multiplicative linear logic | |
multiplicative-exponential linear logic | |
multiprocessor | |
multiscale simulation | |
multiscale simulations | |
multiset comprehension | |
Multiset Rewriting | |
Music | |
Mutability | |
mutable state | |
mutual exclusion protocol | |
MV-algebra | |
MV-algebras | |
N | |
n-dependent theories | |
n-interpolation | |
naive set theory | |
naive truth | |
naive types | |
Narrative | |
Nash bargaining | |
Nash equilibria | |
Nash equilibrium | |
natural deduction | |
Natural duality | |
natural language | |
natural language arguments | |
natural language processing | |
natural logic | |
near semi-rings | |
Need for Cognition | |
Needed step | |
negation | |
negation as failure | |
negation-as-failure | |
Negative translation | |
negative translations | |
neighborhood embedding | |
Neighborhood Semantics | |
nested Petri nets | |
nested sequent calculi | |
nested sequents | |
Nested words | |
network protocol | |
network protocols | |
network rewriting | |
Network security | |
network update | |
networks | |
neurobiology | |
new features | |
NEXPTIME | |
Nice enumerations | |
Noetherian induction | |
Noetherian spaces | |
nominal | |
Nominal Anti-Unification | |
nominal automata | |
Nominal Equivariance Algorithm | |
Nominal Logic | |
nominal schemas | |
nominals | |
Non monotonic reasoning | |
Non-characterizability | |
Non-circular Justifications | |
Non-classical Logic | |
non-classical logics | |
non-convex aggregates | |
non-determinism | |
non-deterministic semantics | |
Non-disjoint union of theories | |
non-elementary classes | |
non-extensional computation | |
non-interference | |
Non-linear | |
non-linear optimization | |
non-linear real arithmetic | |
non-monotonic consequence | |
non-monotonic fixed point theory | |
Non-monotonic Logic Programming | |
non-monotonic logics | |
Non-monotonic reasoning | |
Non-orthogonality | |
non-standard analysis | |
Non-standard inferences | |
non-standard models | |
non-standard reasoning | |
non-termination | |
non-uniform computation | |
Non-uniform inductive types | |
nonconvex subexpression | |
nondeterminism | |
nonexpansive iterations | |
noninterference | |
Noninterleaving semantics | |
Nonlinear Real Arithmetic | |
nonmonotonic logic | |
nonmonotonic reasoning | |
Nonstandard Analysis | |
Nontermination | |
normal forms | |
Normal modal logic | |
normal modal logics | |
Normal multi-modal logics | |
Normalisation | |
Normalisation paths | |
Normalization | |
normalization equivalence | |
Normative reasoning | |
notations | |
NP-completeness | |
Number Restrictions | |
Numbers | |
Numerical Accuracy | |
numerical existence property | |
Numerical representations | |
Nuprl | |
O | |
o-minimality | |
OBDA | |
OBDA design tools | |
OBDD | |
Object Creation | |
Object Oriented Design | |
object-oriented logic programming | |
Object-Oriented Programming | |
Observational Equivalence | |
Observational Semantics | |
Observational Type Theory | |
OCaml | |
omega enumeration degrees | |
Omega-automata | |
omega-stable structure | |
one counter automata | |
one counter nets | |
One-Counter automata | |
online banking | |
ontological queries | |
Ontologies | |
ontologies and linked data | |
ontology | |
Ontology Based Data Access | |
ontology based query answering | |
Ontology Change | |
Ontology Decomposition | |
ontology engineering | |
ontology languages | |
Ontology modularisation | |
ontology modularity | |
Ontology Reasoning | |
Ontology Repair | |
Ontology-based data access | |
Opaqueness | |
open street map | |
Open-Source | |
open/closed world semantics | |
OpenCL | |
operational semantics | |
Optimal Networks | |
Optimal strategy synthesis | |
optimisation | |
optimization | |
optimizing compilers | |
Orbits for functions in finite domains | |
order dimension | |
Ordered | |
Ordered Disjunction | |
Orderings | |
Orders of Magnitude | |
ordinal analysis | |
ordinal foundation | |
ordinal notation system | |
Ordinal notations | |
ordinal number | |
Ordinals | |
ornament | |
orthogonalisation | |
Orthogonality | |
OS FSM model | |
Otter | |
overlay journals | |
OWA and CWA | |
OWL | |
OWL 2 EL | |
OWL 2 profiles | |
OWL 2 QL | |
OWL 2 reasoners | |
OWL 2 RL | |
OWL Reasoner | |
OWLlink | |
P | |
P-compatible identity | |
p-simulation | |
padlock | |
pairwise rendezvous | |
Paracomplete | |
paraconsistency | |
Paraconsistent Logic | |
paraconsistent logics | |
paraconsistent negation | |
Paradox | |
Paradoxes | |
Parallel | |
Parallel Closedness Theorem | |
parallel composition | |
Parallel computation | |
parallel computing | |
parallel deduction | |
parallel evaluation | |
Parallel Local Search | |
parallel materialisation | |
parallel portfolio solver | |
parallel programming | |
Parallel Reasoning | |
Parallel SAT solver | |
parallel satisfiability solver | |
Parallel Solving | |
parallel substitutions | |
Parallelism | |
parallelization | |
parameter estimation | |
parameter synthesis | |
parameter-free induction | |
parameterised verification | |
parameterized communication topology | |
parameterized complexity | |
parameterized model checking | |
parameterized synthesis | |
parametric comonads | |
parametric uniformity | |
Parametrized systems | |
Parikh's theorem | |
parity games | |
Parser | |
part-whole | |
Partial conservativity (of the theory T over the | |
partial correctness | |
partial deduction | |
partial derivatives | |
partial equivalence checking problem | |
Partial Equivalence Relations | |
partial evaluation | |
partial order reduction | |
Partially Observable Markov Decision Processes | |
partially ordered set | |
Partially Ordered Sets | |
passivation | |
Passivization | |
Pastry | |
Path | |
Path Based SCC Algorithms | |
pattern | |
Pattern calculus | |
Pattern matching | |
patterns | |
PCA | |
PCFG | |
PCR | |
PCTL | |
PDL | |
pdr | |
peak decreasingness | |
Pearl's virtual evidence method | |
Pebble walking automata | |
pedagogy | |
peer-to-peer protocols | |
perfect Jonsson theory | |
perfect masking | |
Perfect MV-algebra | |
performance | |
performance evaluation | |
performance prediction | |
Performance-Analysis | |
periodically iterated morphisms | |
Permissive-upgrade | |
Permutation Constraints | |
permutation equivalence | |
Permutation Flowshop Scheduling Problem | |
Permutation lemmas | |
Persistency | |
Personality Traits | |
personalized PageRank | |
Petri nets | |
PGAS | |
pGCL | |
pharmacogenomics | |
Phase Conjugating Mirror | |
phase transitions | |
Phase-bounded | |
Philosophy | |
philosophy of mathematics | |
Physical systems verification | |
PIDE | |
piecewise polynomial functions | |
Pierce-Birkhoff conjecture | |
pigeonhole principle | |
ping-pong protocols | |
PKCS#11 | |
planning | |
Planning and Pseudo-boolean Optimization | |
Planning as Satisfiability | |
planted distribution | |
Plausibility Rankings | |
pocrims | |
pointer arithmetic | |
Pointer Machines | |
polarisation | |
policy composition | |
policy iteration | |
Polish groups | |
Polish structure | |
Polya | |
polyhedral geometry | |
Polymer Reaction Network | |
polymorphic typing | |
polymorphism | |
polynomial | |
polynomial approximations | |
polynomial calculus | |
polynomial constraints | |
Polynomial Contraints | |
Polynomial extension | |
Polynomial Hierarchy | |
polynomial interpretations | |
Polynomial runtime complexity | |
polynomial space | |
polynomial systems | |
polynomial time | |
polynomial time algorithm | |
poplmark | |
population size in relational models | |
Porfolio | |
Portability | |
Portfolio | |
Portfolio Solving | |
Posets | |
Possibilistic networks | |
PosSLP | |
power analysis | |
Power Kripke-Platek set theory | |
Power managment designs | |
PP | |
predicate abstraction | |
predicate discovery | |
predicate transformer | |
Predicative mathematics | |
predicativity | |
predictive analytics | |
Preference | |
Preference based Argumentation | |
preference handling | |
preferences | |
preferences on rules | |
Preferential | |
preferred answer sets | |
prefix grammar | |
prefix probability | |
pregeometries | |
Pregeometry | |
Pregroups | |
premature convergence | |
Preorders | |
preprocessing | |
Presburger arithmetic | |
preservation | |
preservation theorems | |
preserving soundness | |
presheaf | |
Presheaf semantics | |
primal infon logic | |
prime critical pairs | |
prime implicates | |
prime impliquates | |
prime network | |
Primitive Conditional Connective | |
PRISM | |
Privacy | |
Privacy & Information Flow | |
privacy foundation | |
Privacy policy compliance | |
Probabilistic Abstract Interpretation | |
Probabilistic BMC | |
probabilistic classes of computational complexity | |
probabilistic conditional | |
Probabilistic Description Logic | |
Probabilistic grammar | |
Probabilistic hybrid automaton | |
Probabilistic Inductive Logic Programming Statistical Relational Learning | |
probabilistic logic | |
Probabilistic Logic Programming | |
Probabilistic Logic Programs | |
probabilistic logics | |
Probabilistic Model Checking | |
Probabilistic Model Checking Case Studies | |
probabilistic models | |
Probabilistic Program Semantics | |
probabilistic programming | |
probabilistic reasoning | |
probabilistic satisfiability (PSAT) | |
probabilistic systems | |
probability | |
probability box | |
Proble-specific Solver | |
problem libraries | |
ProbLog | |
procedural attachment | |
Procedural knowledge Representation | |
procedural program | |
procedural semantics | |
Process Adaptation | |
process algebra | |
Process Calculi | |
process calculus | |
Process Engineering | |
Process Modelling | |
process visualization | |
producer/consumer model | |
Product logic | |
Product Modal Logics | |
Product Programs | |
Product Update | |
production rule systems | |
PROforma | |
program analysis | |
program debugging | |
program equivalence | |
Program extraction | |
Program Logic | |
program logics | |
program refactoring | |
Program repair | |
program schematology | |
program semantics | |
program specialization | |
program synthesis | |
program transformation | |
program transformations | |
program verification | |
program verification in Coq | |
programmable gates | |
Programmable logic controllers | |
programming | |
programming framework | |
Progression | |
progression of basic action theories | |
Projection | |
projective determinacy | |
projective plane | |
projective unification | |
Prolog | |
Prolog implementation | |
Prolog System | |
Prolog to Java translation | |
proof | |
proof assistants | |
proof automation | |
proof calculus | |
proof checker | |
proof checking | |
proof complexity | |
proof complexity of strong equal tautologies | |
proof compression | |
proof construction | |
proof equivalence problem | |
proof mining | |
proof net | |
proof nets | |
proof nets retraction | |
Proof Obligations | |
Proof of topological properties | |
Proof of total correctness | |
Proof Patterns | |
Proof pearl | |
proof procedure | |
proof procedure language | |
proof search | |
Proof strategy language | |
proof systems of modal propositional logic | |
proof terms | |
proof theory | |
proof-net | |
proof-nets | |
Proof-Patterns | |
proof-search | |
proof-structure | |
Proof-theoretic methods | |
Proof-Theoretic Semantics | |
proof-theory | |
Proofs | |
proofs without syntax | |
PROP | |
PROP quasi-order | |
properties of graph structures | |
property based testing | |
Property Directed Reachability | |
property-driven | |
Property-Driven Reachability | |
propositional assignments | |
propositional closure | |
Propositional dynamic logic | |
propositional logic | |
propositional logics | |
Propositional model counting | |
Propositional Normal Modal logics | |
Propositional proof system | |
Propositional Resolution | |
Propositional Satisfiability | |
ProPPR | |
Protege | |
proto-differential nets | |
proto-net | |
proto-Taylor expansion | |
Protoalgebraic logics | |
protocol analysis | |
Protocol Security | |
Protocol Suite | |
protodisjunction | |
Provability Logic | |
provenance | |
Prover IDE | |
proving | |
Pseudo-algebraically non-separable closed fields | |
pseudo-antichain | |
pseudo-Boolean Constraints | |
pseudofinite | |
pseudorandom constructions | |
PSPACE-complete | |
psychological validation | |
PTIME dialects | |
PTQ-fragment | |
Public key crypto | |
Pudlak rules | |
pure lambda-calculus | |
Pure method calls | |
Pure Nash Equilibria | |
Pure Type Systems | |
pushdown automata | |
Pushdown Systems | |
Q | |
Q-resolution | |
QBF | |
QBF of bounded treewidth | |
QBF-solver | |
Qualified syllogisms | |
qualitative algebras | |
qualitative constraint networks | |
Qualitative reasoning | |
qualitative spatial reasoning | |
quantified Boolean formula | |
Quantified Boolean Formulas | |
quantified constraint satisfaction | |
quantified dynamic logic | |
Quantified Formulas | |
quantifier elimination | |
quantifier instantiation | |
quantifier-free | |
Quantifiers | |
quantifiers and theories | |
Quantitative analysis | |
quantitative information flow | |
Quantitative Model-Checking | |
quantitative objectives | |
Quantitative security | |
Quantitative semantics | |
quantitative synthesis | |
quantitative systems | |
quantum circuits | |
quantum computation | |
Quantum Computing | |
Quantum Flip Gate | |
Quantum Optics | |
Quasi-Invariants | |
quasi-varieties | |
quasiminimal structures | |
quasivarieties | |
Quasivariety | |
quaternion | |
query answering | |
query entailment | |
Query Evaluation | |
query generation | |
query languages | |
query optimization | |
query plan generation | |
query rewriting | |
question answering | |
quickcheck | |
R | |
R-calculus | |
R-Mingle | |
r.e. degrees | |
Ramsey null | |
Ramsey Theorem | |
Ramsey theory | |
Random CNFs | |
random satisfiability | |
random testing | |
random walks | |
Randomized Bubble Sort | |
Randomized Search | |
Randomness | |
rank | |
Ranking Function | |
ranking queries | |
ranking semantics | |
rational closure | |
rational relations | |
Rational Terms | |
rationality | |
RDF | |
RDFS | |
RDMA | |
reachability | |
reachability analysis | |
Reachability assertions | |
reachability games | |
Reachability problem | |
Reaction enumerator | |
Reaction Networks | |
Reactive reasoning | |
reactive synthesis | |
reactive systems | |
real algebra | |
real analyis | |
real analysis | |
real closed exponential field | |
real closed field | |
Real fields | |
real inequalities | |
Real number computation | |
Real Turing Machine | |
real-time | |
real-time systems | |
real-time verification | |
realizability | |
Realizability semantics | |
realization | |
reals | |
reasoner | |
reasoner performance | |
reasoners | |
Reasoning | |
reasoning about action and change | |
reasoning about actions | |
Reasoning about Actions and Change | |
reasoning about contexts | |
reasoning about knowledge and action | |
reasoning about knowledge and belief | |
Reasoning in Fiction | |
Reasoning under uncertain inputs | |
Reconfiguration | |
reconfiguration problem | |
Recurrence relation | |
Recurrent Clustering | |
recursion | |
recursion schemata | |
Recursion Schemes | |
recursion theory | |
Recursive path ordering | |
recursive tactics | |
Recursive Types | |
reducibility | |
Reduct | |
reductio ad contradictionem | |
reduction to SAT | |
Reductions | |
Reductions to SAT | |
redundancy | |
Reference | |
refinement | |
Refinement Modal Logic | |
refinement relation | |
Refinement types | |
refinement-based verification | |
Refining partial structures | |
reflection | |
Reflection principle | |
reflection principles | |
Refutation | |
region connection calculus | |
Region logic | |
Regional Energy Planning | |
regression test selection | |
regression verification | |
Regular cost functions | |
regular expression equivalence | |
regular expressions | |
Regular formulas | |
regular languages | |
Regular Languages of Infinite Words | |
Regular Languages of Words | |
regular path queries | |
relational | |
relational conditional | |
Relational dual tableau system | |
relational logic | |
relational logistic regression | |
relational probabilistic models | |
relational semantics | |
Relationship between deduction methods | |
relative clauses | |
relative error | |
relative termination | |
relativity theory | |
relaxation | |
relaxed instance queries | |
relaxed memory models | |
Relaxed Queries | |
Relevance | |
relevance logic | |
relevance logics | |
Relevance Theory | |
relevant logic | |
reliable constraint reasoning | |
remote code execution | |
renaissance geometry | |
Reordering | |
Repair Decomposition | |
Repairing | |
representative agent | |
requirement traceability | |
residual number system | |
residuated frames | |
Residuated lattice | |
Residuated lattices | |
resolution | |
resolution and superposition | |
resolution complexity | |
Resolution Method | |
Resolution rules | |
resolution space | |
resolution width | |
Resource lambda-calculus | |
resource sensitive logics | |
Resource Usage Analysis | |
Resource λ-calculus | |
resource-bounded search | |
Restrictiveness | |
Retyping functions | |
reverse mathematics | |
Reversible computing | |
revision | |
revision calculus | |
rewards | |
Rewrite Systems | |
Rewriting | |
Rewriting in action logic | |
rewriting logic | |
Rewriting system | |
rewriting techniques | |
rhythm representation | |
rich | |
risk | |
Risk Awareness | |
risk communication | |
risk mitigation | |
Risk Propensity | |
RL systems | |
robot protocols | |
Robotics | |
Robots | |
robust quantitative objectives | |
Roger semilattice | |
Rogers semilattice | |
Rough DL | |
rough sets | |
round model | |
Routley-Meyer semantics | |
RTL | |
rule safety | |
Rule transposition | |
rule-based modeling | |
rule-based models | |
Rule-Labelling | |
rules | |
runtime analysis | |
Runtime Complexity | |
Runtime Complexity Analysis | |
Runtime monitoring | |
runtime verification | |
Russell's Paradox | |
S | |
s | |
safe recursive set functions | |
Safety | |
Safety relation | |
safety-critical real-time systems | |
Safety-critical systems | |
SAT | |
SAT application | |
SAT competitions | |
SAT encoding | |
SAT encoding of combinatorial problems | |
sat encodings | |
SAT Features | |
SAT modulo theories | |
SAT partitioning | |
SAT platform | |
SAT proofs | |
SAT solver | |
SAT solvers | |
SAT solving | |
SAT under Assumptions | |
SatELite | |
Satifiability Modulo Theory | |
satisfiability | |
Satisfiability in Alternating-time Temporal Logic | |
Satisfiability Modulo Theories | |
Satisfiability problem | |
Satisfiability procedure | |
saturation | |
saturation algorithm | |
Saturation Algorithms | |
Saturation Procedures | |
Saucy | |
Scala | |
Scalability | |
Scalable Unbounded Verification | |
scalar extension property | |
scalar implicature | |
scale-free networks | |
scattered linear order | |
Sceptical reasoning | |
scheduling | |
Schematic Proof | |
Science Popularization | |
Scope-bounded | |
Scope-Bounding | |
Scott data types | |
Scott-continuous function | |
Scrap Your Boilerplate | |
Scripting Language | |
scripting languages | |
Sea Urchin Development | |
search | |
search problems | |
second order logic | |
second-order arithmetic | |
second-order Godel logic | |
second-order logic | |
Second-order quantifier elimination | |
secrecy | |
secret-sharing | |
Secure Electronic Voting | |
secure equilibria | |
secure multi-execution | |
Secure multiparty computation | |
secure services | |
secure sets | |
Secure Web Bulletin Board | |
Security | |
Security API | |
security APIs | |
Security Awareness | |
Security Ceremonies | |
security in graphs | |
Security lattice | |
Security models | |
security policy | |
security properties | |
security protocols | |
Security Type Systems | |
security vulnerabilities | |
self organization | |
self regulation | |
Self-learning | |
self-modifying programs | |
Self-reference | |
Self-similarity | |
self-stabilization | |
selfextensional logics | |
semantic entailment | |
semantic guidance | |
semantic information | |
semantic knowledge | |
semantic labelling | |
semantic model | |
semantic paradoxes | |
semantic rewriting | |
Semantic tableaux | |
Semantic Web | |
Semantic Web and Natural Language Processing | |
Semantic Web of Things | |
semantics | |
Semantics and pragmatics | |
Semantics of Aggregates | |
Semantics of Conditional Literals | |
Semantics preservation | |
Semantics-Based Program Transformation | |
semi-formal specification | |
semi-orders | |
semi-ring computation | |
semi-Thue system | |
semialgebraic | |
Semigroups | |
semilattice | |
Semilattice Polymorphisms | |
semilattices | |
Semimodule | |
semisimple MV-algebras | |
separation | |
Separation algebras | |
separation kernel | |
separation kernels | |
separation logic | |
sequence of sat | |
Sequences of small discrepancy | |
sequent calculi | |
sequent calculus | |
sequent-based systems | |
sequential consistency | |
sequential decision problems | |
sequential theories | |
Sequentialization | |
Sequents of Relations | |
Session integrity | |
session log | |
session types | |
set arithmetic | |
Set Comprehension | |
set functions | |
set theory | |
set-based theorems | |
Set-theory | |
sets | |
Sets with atoms | |
shape analysis | |
shared-memory | |
Shatter | |
sheaf | |
sheaf model | |
Sheaf semantics | |
Sherali-Adams | |
SHOIQ | |
SHOQ | |
Short Paper | |
Shortest Path | |
SHQ | |
shuffle | |
side channel attacks | |
Side-effects | |
Sigma-definability | |
Sigma-predicate | |
Signal-Flow-Graphs | |
silent transitions | |
similarity | |
similarity measures | |
Simple theories | |
Simple Theory of Types | |
simplex | |
simply typed lambda calculus | |
simply-typed lambda-calculus | |
simulation | |
Simulation and alternating simulation | |
simulations | |
singleton arc consistency | |
situation calculus | |
size | |
Skolem/Herbrand function | |
Skolemization | |
SLD-resolution | |
SLS | |
smart card | |
Smart Cities | |
Smart Health | |
SMT | |
SMT solvers | |
SMT solving | |
SMT-LIB | |
SMT-solving | |
SNOMED-CT | |
Social Choice | |
social choice theory | |
Social Engineering | |
Social Network Theory | |
Socio-Technical Security | |
socratic proofs | |
Soft Constraints | |
software defined network | |
software description | |
software design patterns | |
Software Fault Isolation | |
software model checking | |
Software Science | |
Software synthesis | |
software test | |
software testing | |
software toolkit | |
Software Verification | |
solvability/unsolvability of problems | |
Solver | |
Solver competitions | |
Solver Construction | |
Solver execution services | |
Solvers | |
solving | |
Sorites | |
sorted signature | |
Sound | |
Sound Abstraction | |
soundness | |
Source code classification | |
Source-to-Source Transformation | |
SPA | |
space | |
SPARQL | |
SPARQL Update | |
SPASS | |
Special cases of MP | |
specification | |
specification debugging | |
specification patterns | |
Specification Synthesis | |
Specification Testing | |
Specifications | |
specificity | |
spectra | |
spectra of structures | |
spectral space | |
speech act theory | |
splittiing | |
SROIQ | |
SSA Form | |
SSH | |
SSReflect | |
stability | |
stability analysis | |
stable model semantics | |
Stable Models | |
Staged Computation | |
Standard completeness | |
standard completness | |
standard reasoning | |
Standards | |
state space analysis | |
State-boundedness | |
statecharts | |
Static Analysis | |
static checking | |
statistical information | |
Statistical Relational Artificial Intelligence | |
Statistical Relational Learning | |
STD | |
step-indexing | |
step-wise refinement | |
stochastic chemical kinetics | |
Stochastic Logic Programs | |
stochastic processes | |
Stochastic satisfiability modulo theories | |
Stochastic shortest path | |
Stone duality | |
Stone-Priestley duality | |
Store buffer reduction | |
Story Comprehension | |
Story Telling | |
story understanding | |
straight-line program | |
strand spaces | |
Strategic Environmental Assessment | |
strategic interaction | |
strategies | |
Strategies for dialogical argumentation | |
strategy development | |
Strategy Logic | |
stream transducer | |
streams | |
string | |
string constraints | |
string processing | |
string rewriting | |
String solvers | |
String transducers | |
strings | |
Strong Embedding | |
Strong Entailment | |
strong equality of modal tautologies | |
strong equivalence | |
strong negation | |
Strong normalisation | |
strong normalization | |
strong termination | |
Strong Update | |
Strongest Necessary Conditions | |
Strongly Connected Components | |
structural completeness | |
structural decompositions | |
structural equations | |
Structural tractability | |
Structurally completeness | |
structure | |
structure learning | |
Structure preserving | |
structured code generators | |
structured proof | |
structures of bounded degree | |
stuttering bisimulations | |
sub-classical logics | |
Sub-formula Property | |
subdirectly irreducible algebras | |
subexponential | |
subgame perfect | |
subrecursive degrees | |
subset-simulation | |
substitutability | |
substitution | |
substructural logic | |
substructural logics | |
Substructural predicate logics | |
Substructural Types | |
subsumption | |
Subterm selection | |
subtyping | |
subvarieties | |
subword complexity | |
Succinctness | |
sudoku puzzle | |
Sunburst Tree | |
supercompilation | |
superposition | |
superposition calculus | |
superstability | |
support function | |
supported model semantics | |
Surveillance | |
Suszko operator | |
switch | |
symblicit approach | |
Symbolic analysis | |
Symbolic Automata | |
symbolic computation | |
symbolic execution | |
Symbolic model | |
Symbolic Model Checking | |
symbolic orthogonal projections | |
symbolic simulation | |
Symbolic Time bounds | |
symbolic transducers | |
symmetric encryption | |
symmetric indivisibility | |
Symmetric monoidal categories | |
Symmetry | |
synaptic vesicle cycle | |
Syntactic cut-elimination | |
syntax-semantics interface | |
synthesis | |
synthetic biology | |
System Architecture | |
System description | |
System F | |
System T | |
Systematic Testing | |
SystemC | |
Systems Biology | |
T | |
Tableau | |
Tableau Algorithm | |
Tableau Algorithms | |
tableau reasoning | |
tableau systems | |
Tableau-based Decision Methods | |
tableaux | |
Tableaux calculi | |
tableaux calculus | |
tabled abduction | |
Tabling | |
tactics | |
tactics and tacticals | |
tag systems | |
tagged hardware | |
tame structures | |
Tarski | |
task planning | |
Taylor expansion | |
taylor series | |
TBox Revision | |
TC_0 | |
teaching | |
technical vision | |
Technology Adoption | |
telecommunication protocol | |
Temperature puzzle | |
template iterations | |
templates domain | |
temporal attributes | |
Temporal Description Logics | |
temporal logic | |
temporal logics | |
Temporal projection | |
temporal querying | |
Temporal Reasoning | |
temporal stable models | |
tensor algebra | |
tensor product | |
Tensorial logic | |
Term | |
term algebra | |
term indexing | |
term ordering | |
term representation | |
Term Rewrite Systems | |
term rewriting | |
Term rewriting system | |
Term Rewriting Systems | |
Term Size Analysis | |
terminal semantics | |
termination | |
termination analysis | |
Termination proof | |
Termination Theorem | |
terminologies | |
termspace forcing | |
test data generation | |
testing | |
textual entailment | |
teyjus system | |
tgds | |
the B I monoid | |
the bar induction | |
The Correctnes Of Transformations | |
The dependency pair framework | |
the game of Alonzo | |
the pcp theorem | |
The theory of subsets of $\omega_1$ | |
theorem prover | |
theorem prover technology | |
theorem provers | |
theorem proving | |
theorem-prover implementation | |
Theorem-Proving | |
Theorema | |
Theories of interpretation | |
Theory approximation | |
Theory combination | |
theory of almost sure validities | |
Theory of arrays | |
Theory of Play | |
Theory of Strings | |
theory S relative the class of formulae C) | |
Threat models | |
Three-value logic | |
Three-valued logic | |
Three-valued Lukasiewicz Logic | |
three-valued semantics | |
Three-valued Łukasiewicz Logic | |
tiling problem | |
time | |
Time Travel | |
timed automata | |
timed transition systems | |
timed verification | |
timing analysis | |
Timing Attacks | |
Timing of Security Decisions | |
TLA | |
TLA+ | |
TLB | |
TLS | |
token | |
token machines | |
token-passing systems | |
Tool | |
Tool description | |
Tool paper | |
tool support | |
Tools | |
top-down query-answering | |
topological dynamics | |
Topological vector spaces | |
topology | |
Topos theory | |
Tor | |
Total Space | |
TPTP | |
TPTP process Instruction language | |
tracing | |
tractability boundaries | |
tractability theory | |
Tractable Classes | |
Training of HC professionals in differential diagnosis | |
Trakhtenbrot theorem | |
transaction | |
transaction logic | |
transactions | |
Transfer | |
transfer of meta-theory | |
transfer theorem | |
transfinite reduction | |
transformation | |
Transformation Analysis | |
transformation system | |
Transformations | |
transformer | |
transition system | |
Transitive closure | |
Translation | |
translation validation | |
translations | |
TReasoner | |
tree automata | |
tree automaton | |
Tree-Automata | |
trees | |
treewidth | |
trimming | |
Trip Count Prediction | |
true concurrency | |
Trust | |
Truth | |
truth predicates | |
Truth-equational logics | |
Tukey | |
tuple | |
tupled pregroup grammars | |
Tupling | |
Turing machine | |
Turing machines | |
Turing operator | |
Turing reducibility | |
Turing's Halting Problem | |
Turing-computable embedding | |
tutorial | |
twelf | |
two-dimensional partial map | |
two-player games | |
two-player games on weighted graphs | |
two-variable logic | |
two-variable logics | |
two-way automata | |
Type | |
Type and effect system | |
Type Classes | |
Type containment | |
type framework | |
type inference | |
Type Introduction | |
type isomorphism | |
type preservation | |
type system | |
Type systems | |
type theory | |
type-based theorems | |
type-directed editing | |
typeclasses | |
Typed lambda calculus | |
typed lambda-calculus | |
types | |
typical-case complexity | |
typing | |
U | |
Ubiquitous computing | |
UD-randomness | |
ultimately-periodic sets | |
ultrafilter | |
unary regular language | |
uncertainty | |
Uncertainty Reasoning | |
undecidability | |
unfolding | |
Unfolding graph rewriting | |
unfoldings | |
Unification | |
Unification type | |
uniform continuity | |
uniform distribution | |
Uniform Interpolation | |
Uniform interpolation and forgetting | |
uniform iterativity | |
uniform termination | |
uniformity | |
Uniformization | |
Uniformization Rule | |
unifying theories of programming | |
Uninorm Logic | |
unintentional | |
Union of non-disjoint theories | |
Universal algebra | |
Universal composability | |
universal numbering | |
universal translation | |
universally definable | |
universe polymorphism | |
universes | |
unraveling | |
Unravelings | |
unsatisfiability proof | |
unwinding relation | |
up-to techniques | |
update | |
updates | |
upper bound | |
Upper bounds | |
Upper Complexity Bounds | |
upper powerdomain | |
Usability | |
usable rules | |
Usable Security | |
Use cases and deployments of computerized guidelines and protocols with EPRs | |
user interface | |
user interfaces | |
user interfaces for interactive theorem provers | |
user perception | |
Users | |
Utility Theory | |
V | |
vagueness | |
Validation | |
Validation of Numerical Programs | |
validity | |
Vampire | |
variable bindings | |
Variable Dependencies | |
Variable Elimination | |
Variational Bayes | |
varieties | |
variety | |
VASS | |
Vaught's conjecture | |
VCG | |
vector addition systems | |
Vector Space Semantics | |
verification | |
verification condition generator | |
Verification conditions | |
verification of object code | |
verification of requirement specification | |
verification tools | |
verificiation | |
verified RTOS | |
Verified Software | |
Verified verifiers | |
verifying compiler | |
veriT | |
viability | |
Vickrey's theorem | |
Video Games | |
Virtual Characters | |
virtual machine | |
virtual substitution | |
virtual term substitution | |
Visible strategies | |
Visibly Pushdown Languages | |
visual and spatial cognition and computation | |
Visual Languages | |
Visual query formulation | |
Visual query formulation interface | |
visualization | |
von Neumann's Minimax theorem | |
vulnerability | |
W | |
W[2]-hardness | |
Wadge-like hierarchies | |
Wave-style Token machines | |
weak arithmetic | |
weak circular minimality | |
Weak Completion Semantics | |
weak constraints | |
weak EXP hierarchy | |
weak memory | |
Weak Memory Models | |
weak monadic second-order | |
weak normalization | |
weak pigeonhole principle | |
Weak relevant model structures | |
weak simulation | |
weakly implicative logic | |
weakly shallow | |
Web authentication | |
Web of Linked Data | |
web programming | |
web scripts | |
web service choreography | |
Website Fingerprinting | |
weight | |
Weighted first-order logic | |
Weighted Model Counting | |
weights | |
Weihrauch degree | |
Weihrauch reducibility | |
well-founded model | |
Well-Founded Semantics | |
Well-structured pushdown systems | |
well-supported models | |
wellorder | |
while-programs | |
width | |
Wiener measure | |
Winograd Schema Challenge | |
Winograd Schemas | |
witness | |
WMSO | |
word equations | |
word-level model checking | |
Workflow | |
world view | |
wqo theory | |
wrap ambiguity | |
WWKL | |
X | |
XML | |
XML and graph data | |
XML Processing | |
XML Schema | |
XOR-SAT | |
xpath | |
XSB Prolog | |
XSD | |
Y | |
Yablo's Paradox | |
Z | |
Z-Transform | |
Zeno’s paradoxes | |
zero-knowledge proofs | |
zero-one laws | |
Σ | |
Σ^0_2-sets |