This document complements the other "kowledge management" related files, e.g. the general 'Semantic Classification of Knowledge Management Resources', the 'Semantic Classification of Formal Concept Analysis Resources' and the 'Semantic Classification of Conceptual Graph Resources'. However, for now, this file only has the first section ("Domains and Theorie"). It also only use the ">part" and "url" links. Other links will be used later. (This is just a beginning).
The generic user "km" is used below. Since this is a "generic user", no password is (and can be) associated to it in WebKB-2, and anyone may add categories in this name.
Reminder: (i) the link "object" has different (more specialized) meanings depending on the connected categories, (ii) so does the link "part": between physical objects it refers to the link "physical part", between tasks it refers to the link "subtask".
WordNet has two categories for "logic": #logic.philosophy refers to a "field of study" and #system_of_logic refers to a particular kind of system (and hence of collection). In our ontology, #system_of_logic is a concept type while fields of study are individuals organised by links ">part" (subdomain) and, like theories, are interpreted as "one or several propositions" (one proposition may be composed of sub_propositions). Below, we develop the hierarchy of fields of study below #logic.philosophy. In the low-level of these hierarchies are particular theories which could be represented as instances of #system_of_logic (in these cases, with this representation, the field of study can be nothing more that the theory itself). WordNet gives a few specializations to #system_of_logic which may be interpreted both as theories and fields of study (e.g. #Aristotlean_logic and #propositional_logic); hence, in our integration of WordNet, we have represented these specializations as instances (not subtypes; WordNet does not make the difference) and re-used their identifiers in the classification of fields of study below.
Similarly, an individual km#semantics_of_logic is introduced to represent the field of study "semantics of logic". A type km#semantic_of_logic could be introduced to
What is represented below is my interpretation of the documents
accessible from
http://en.wikipedia.org/wiki/Logic.
Some parts are probably incorrect (e.g. I commented the part about
"application_of_mathematical_techniques_to_formal_logic" because
I am unsure about it). In a short while, the interface of WebKB-2
will include a knowledge-oriented wiki system to permit users to update
pages such as this one but for now, if you have corrections or additional
representations, thanks for mailing them to me (e.g. by sending a
corrected file).
km#semantics_of_logic (^approaches that logicians have introduced to understand and determine that part of meaning in which they are interested; the logician traditionally is not interested in the sentence as uttered but in the proposition, an idealised sentence suitable for logical manipulation^)
>part of: #semantics,
>part: km#model-theoretic_semantics km#proof-theoretic_semantics,
url: http://en.wikipedia.org/wiki/Semantics_of_logic;
km#model-theoretic_semantics (^the most widepsread approach, and is based on the idea that the meaning of the various parts of the propositions are given by the possible ways we can give a recursively specified group of interpretation functions from them to some predefined mathematical domains: an interpretation of first-order predicate logic is given by a mapping from terms to a universe of individuals, and a mapping from propositions to the truth values "true" and "false"^);
km#proof-theoretic_semantics (^approach associating the meaning of propositions with the roles that they can play in inferences^)
url: http://en.wikipedia.org/wiki/Proof-theoretic_semantics;
#logic.philosophy
//a field of study; the purpose of a logic is to characterize the difference between valid and invalid arguments
>part: km#inductive_reasoning_system km#deductive_reasoning_system
km#binary_logic km#multi-valued_logic
km#informal_logic km#formal_logic,
url: http://en.wikipedia.org/wiki/Logic;
km#inductive_reasoning_system (^study of deriving a "reliable" ("inductively valid") generalization from observations^);
km#deductive_reasoning_system (^an inference is "deductively valid" if and only if there is no possible situation in which all the premises are true and the conclusion false^);
km#binary_logic__boolean_logic (^logic where the principle of bivalence is respected; this principle states that for any proposition P, either P is true or P is false^)
url: http://en.wikipedia.org/wiki/Binary_logic;
km#multi-valued_logic__many-valued_logic (^logic in which there are more than two possible truth values^)
>part: km#fuzzy_logic km#probability_logic,
url: http://en.wikipedia.org/wiki/Multi-valued_logic;
km#informal_logic (^study of logic as used in natural language arguments^);
km#formal_logic
>part: km#philosophical_logic km#mathematical_logic
km#non-modal_logic km#modal_logic
km#classical_logic km#non_classical_logic
km#type_theory km#term_logic km#dialectical_logic,
url: http://en.wikipedia.org/wiki/Formal_logic;
km#philosophical_logic (^deals with formal descriptions of natural language and hence philosophical logicians have contributed a great deal to the development of non-standard logics^)
//shares much of the ">part" of km#mathematical_logic; left implicit here
url: http://en.wikipedia.org/wiki/Philosophical_logic;
km#mathematical_logic__symbolic_logic__metamathematics //(last name is obsolete)
>part of: km#abstract_algebra,
>part: km#application_of_techniques_of_formal_logic_to_mathematics
km#application_of_mathematical_techniques_to_formal_logic
km#sentential_logic km#predicate_logic
km#logic_for_reasoning_about_computer_programs,
url: http://en.wikipedia.org/wiki/Mathematical_logic;
km#application_of_techniques_of_formal_logic_to_mathematics
>part: km#logicism;
km#logicism (^pioneered by philosopher-logicians such as Gottlob Frege and Bertrand Russell: the idea was that mathematical theories were logical tautologies, and the programme was to show this by means to a reduction of mathematics to logic. The various attempts to carry this out met with a series of failures, from the crippling of Frege's project in his Grundgesetze by Russell's Paradox, to the defeat of Hilbert's Program by Gödel's incompleteness theorems; however, every rigorously defined mathematical theory can be exactly captured by a first-order logical theory; Frege's proof calculus is enough to describe the whole of mathematics, though not equivalent to it^);
/* km#application_of_mathematical_techniques_to_formal_logic
>part of: km#proof_theory km#model_theory km#axiomatic_set_theory km#recursion_theory;
km#proof_theory__calculus (^study of the part of a logical system which determines how to construct arguments: to derive conclusions from premises; it is a set of axioms (which may be an empty set), and a set of inference rules for deriving new well-formed formulas (wffs) from a given set of wffs; it must thus include or be defined in terms of a formal grammar, which will state all of the allowable expressions, the wffs, in the language; any grammar will in general also be given a semantics, which explains those features (truth, implication) that are, presumably, of interest; ideally the axioms and inference rules of a calculus are chosen such that if the formulas in a set are semantically true then any formulas derivable from them are also true; hence a calculus is formulated independently of a semantics, but with the aim of agreeing with it^);
km#model_theory (^study of the representation of mathematical concepts in terms of set theory, or the study of the models which underlie mathematical systems^)
object: km#model-theoretic_semantics;
km#axiomatic_set_theory (^mathematical theory of sets^);
km#recursion_theory__computability_theory (^part of the theory of computation dealing with which problems are solvable by algorithms (equivalently, by Turing machines), with various restrictions and extensions^)
*/
km#sentential_logic__propositional_logic__propositional_calculus (^proof theory for reasoning with propositional formulas as symbolic logic; it is extensional^);
km#predicate_logic__predicate_calculus (^permits the formulation of quantified statements such as "there is at least one X such that..." or "for any X, it is the case that...", where X is an element of a set called the domain of discourse^)
>part: km#FOL km#HOL,
url: http://en.wikipedia.org/wiki/Predicate_logic;
km#FOL__first-order_logic__first-order_predicate_calculus__predicate_logic (^FOL is distinguished from HOL in that it does not allow statements such as "for every property, it is the case that..." or "there exists a set of objects such that..."; it is a stronger theory than sentential logic, but a weaker theory than arithmetic, set theory, or second-order logic; it is strong enough to formalize all of set theory and thereby virtually all of mathematics^)
>part: km#PCEF_logic; //+ km#first-order_theory;
km#PCEF_logic__logic_of_positive_conjunctive_existential_formulas;
// km#first-order_theory (^theory that can be axiomatised as an extension of FOL by adding a recursive set of first-order sentences as axioms^)
km#HOL__higher-order_logic (^based on a hierarchy of types^);
km#logic_for_reasoning_about_computer_programs
>part: km#Hoare_logic
km#logic_for_reasoning_about_concurrent_processes_or_mobile_processes
km#logic_for_capturing_computability;
km#logic_for_reasoning_about_concurrent_processes_or_mobile_processes
>part: km#CSP km#CCS km#pi-calculus;
km#logic_for_capturing_computability
>part: km#computability_logic;
km#non-modal_logic__extensional_logic (^as opposed to intensional logics, the truth value of a complex sentence is determined by the truth values of its sub-sentences^);
km#modal_logic__intensional_logic (^sentences are qualified by modalities such as possibly and necessarily; both "Bush is president" and "2+2=4" are true, yet "Necessarily, Bush is president" is false, while "Necessarily, 2+2=4" is true^)
>part: km#deontic_logic km#epistemic_logic km#temporal_logic km#conditional_logic,
url: http://en.wikipedia.org/wiki/Modal_logic http://plato.stanford.edu/entries/logic-modal/;
km#temporal_logic (^system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time^)
>part: km#tense_logic km#computational_tree_logic__CTL km#linear_temporal_logic,
url: http://en.wikipedia.org/wiki/Temporal_logic;
/* Linear Temporal Togic is a "subset of" Computational Tree Logic,
like FOL is a "subset of" HOL, but there does not seem to be a subdomain relation
between these fields of study. May be this form of "subset of" could be
represented by a "part of" relation, provided this is the sole/main kind of
"part of" relation between theories.
*/
km#non-classical_logic__intuitionist_logic
>part: km#substructural_logic km#paraconsistent_logic km#natural_deduction
km#intuitionistic_logic;
km#substructural_logic (^system of propositional calculus that are weaker than the conventional one^)
>part: km#relevance_logic km#linear_logic,
url: http://en.wikipedia.org/wiki/Intuitionistic_logic;
km#relevance_logic__relevant_logics (^systems developed as attempts to avoid the paradoxes of material and strict implication^)
url: http://plato.stanford.edu/entries/logic-relevance/;
km#paraconsistent_logic
>part: km#relevance_logic km#many-valued_logic km#non-adjunctive_logic;
km#natural_deduction
url: http://en.wikipedia.org/wiki/Natural_deduction;
km#intuitionistic_logic__constructivist_logic (^logic used in mathematical intuitionism and other forms of mathematical constructivism^)
url: http://en.wikipedia.org/wiki/Intuitionistic_logic;
km#type_theory (^branch of mathematics and logic that concerns itself with classifying entities into sets called types^)
url: http://en.wikipedia.org/wiki/Type_theory;
km#term_logic__traditional_logic
>part: #Aristotelian_logic;
#Aristotlean_logic__Aristotelian_logic__syllogistic
url: http://en.wikipedia.org/wiki/Aristotelian_logic
http://plato.stanford.edu/entries/aristotle-logic/;