The formal language of propositional logic. Semantic rules. Calculating the truth-value of propositional formulas. The truth table. Semantic tree. The theory of evidence. Clauses and normal forms. The algorithm of Davis and Putnam. The principle of resolution. Non- clausal resolution. The theorem on compactness. First-order logic. Language. Prenex normal forms. Skolemov forms. Clausal form. Herbrand’s theorem. Resolution in first order logic. Deletion of strategies. Methods of matrix proof. Axiomatic systems. Clarity and completeness of propositional logic. Natural deduction. Predicate calculus. Evidence, models, algorithms and computability. Knowledge representation. The logical representation. Production systems. Representation of networks. Frames. Conceptual graphs. Object data model and database system. Deductive bases. The semantics of deductive databases. The definitive base. Negation. Trivalent logic. Nonmonotonic reasoning. Standard logic. Model inference that can be revised. McDermott nonmonotonic logic. Auto epistemology logic. Concluding under conditions of uncertainty. Probability theory. Network of beliefs. The theory of Dempster and Shaffer. Probabilistic logics. Modal logics. Propositional modal logic. Valuation and tautology. The theory of proof. Multimodal languages. Methods of evidence in modal logic. Proof by resolution. Translation in clausal forms. Methods of proof using a chart. The temporal logic. Requirements of temporal logic. The temporal logic in time of branching. Limited and unlimited time. Linear time. Gusto time. The temporal logic based on dense time. The temporal modal first-order logic. Meta-systems. Meta-programming. Representation of types. Meta-logical predicates. Meta-interpreter.