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