Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Informatică
Programul de studii: Informatică - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MIF0001	Mathematical Foundations of Computer Science	

Semester	Hours: C+S+L	Category	Status	
1	2+2+0	fundamental	compulsory	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
LUPEA Mihaiela	Ph.D.	Lect.	Programming  Languages and Methods	*	*		

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
The aim of the course is the presentation of logical foundations of computer science: propositional and predicate calculus, theorem proving methods, boolean algebras and boolean functions. The connection with logic programming and logical circuits is presented. Additionally, notions related to information representation are introduced.

IV. Course contents
1.	Numeration systems: representation, operations (algorithms for comparison,  addition, subtraction, multiplication, division), conversions between bases. Numbers representation: integers (unsigned, signed – direct, inverse, complementary codes), real numbers (fixed-point representation, floating point representation).

2.	Propositional and predicate calculus from an algebraic point of view and as deductive systems. Normal forms. Decidability problem in propositional and predicate calculus. Direct and refutation proof methods (Herbrand method, resolution method, sequent calculus method, semantic-tableaux method). Formalization of common-sense reasoning and mathematical reasoning using these classical logics. 

3.	Boolean algebras, boolean functions and their applications. Canonic and maximal monoms. Simplification of boolean functions using Veitch, Mc.Quine and Moisil methods. Combinational and sequential logical circuits. 

V. Bibliography
1.	M. Ben-Ari: Mathematical Logic for Computer Science, Ed. Springer, 2001. 
2.	F.Boian, Bazele Matematice ale Calculatoarelor, Editura Presa Universitara Clujeana, 2002 – library.
3.	C.L.Chang, R.C.T.Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press.
4.	M. Cocan, B. Pop: Bazele matematice ale sistemelor de calcul, Editura Albastra, Cluj-Napoca, 2001 – library.
5.	M.Fitting: First-order logic and Automated Theorem Proving, Ed.Springer Verlag, 1990.
6.	M.Lupea: Propositional logic and first-order logic, electronic format, 2006.
7.	Mihaela Malita, Mircea Malita, Bazele Inteligentei Artificiale, Vol. I, Logici propozitionale, Ed. Tehnica, Bucuresti, 1987 – library. 
8.	L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, on-line course.
9.	M. Possega: Deduction Systems, Inst. of Informatics, 2002, on-line course.
10.	 D.Tatar: Inteligenta artificiala: demonstrare automata de teoreme si NLP, Ed. Microinformatica, 2001 – library.
11.	 D.Tatar: Bazele matematice ale calculatoarelor, edition 1999- library.

VI. Thematic of didactic activities per weeks
Lectures 1-2 + Seminars 1-2:
Numeration bases, information encoding, numbers representations
•	Numeration systems:
1.	Definitions, representation and operations (algorithms for comparison, addition, subtraction, multiplication division to a digit) of numbers in a base b. 
2.	Conversions between bases using the methods (calculus in the source base, calculus in the destination base, using an intermediate base) for integer and rational numbers.
3.	Examples for particular bases: 2,3,4,6,8,16.
•	Numbers representation
   1. Representation for unsigned integers, operations (!!overflow!!), algorithms for multiplication and 
       division.
    2. Representation  for signed integers: direct code, inverse code, complementary code, 
    operations(!!overflow!!) and subunitary convention. 
  3. Representations for real numbers: fixed-point representation, floating-point representation (subunitary normalized mantise and the mantise >1). 

Propositional logic
Lecture 3 + Seminar 3:
1.	Syntax (connectives, formulas) of propositional logic.
2.	Semantics: interpretation, model, consistent formula, inconsistent formula, tautology, logical consequence; truth table – a direct proof method.
3.	Laws (logical equivalences): DeMorgan, absorption, commutativity, associativity, distributivity, idempotency.
4.	Clauses and normal forms: conjunctive normal form (CNF) and disjunctive normal form (DNF), algorithm for transformation of a formula into DNF and CNF.
5.	Exercises: 
•	Using the truth table, decide if a formula is consistent/tautology/inconsistent and write all the models for a consistent formula.
•	Transform a formula into DNF and CNF equivalent forms and using these forms decide if a formula is inconsistent/tautology.

Lecture 4 + Seminar 4:
1.	Formal (axiomatic) system associated to propositional logic, deduction, theorem.
2.	Theorem of deduction and its consequences.
3.	Theorem of soundness and theorem of completeness for propositional logic; noncontradiction, coherence and decidability of propositional logic.
4.	Exercises:  
•	Apply the theorem of deduction to prove syllogism rule, separations of premises rule, reunion of premises rule. 
•	Using the axiomatic system prove that a propositional formula is a theorem.

Lecture 5 + Seminar 5:
Semantic tableaux method – a refutation and semantic proof method.
1.	Classes of formulas, decomposition rules, branch (open, closed), construction of a semantic tableau. 
2.	Theorem of soundness and completeness for this method.
3.	Exercises: 
•	From the semantic tableau associated to a propositional formula, write all the models of it.
•	Check if a propositional formula is a tautology / logical consequence of a set of formulas.

Lecture 6 + Seminar 6: 
Sequent calculus - a direct proof method.
1.	The formal system of sequent calculus: sequent, basic sequents, true sequent, sequent inference rules, inference, reduction of a sequent.
2.	Theorem of soundness and completeness for this method.
3.	 Exercises: Check if a propositional formula is a theorem/deductible from a set of formulas using sequent calculus method.

Lectures 7-8 + Seminaries  7-8:
Resolution – a refutation proof method for propositional logic
1.	Resolution as a formal system, theorem of soundness and completeness.
2.	Refinements of resolution: level saturation strategy, set-of–support strategy, deletion strategy, lock resolution, linear  resolution.
3.	Exercises: 
•	Using resolution check if a set of clauses is inconsistent or not.
•	Check if a propositional formula is a theorem/ deductible from a set of formulas using resolution or one of its refinements.

Predicate (first-order) logic
Lecture 9 + Seminar 9:
1.	Syntax: connectives, quantifiers, terms, atoms, formula, clause, literal, closed formula, free formula, the formal (axiomatic) system associated;
2.	Semantics of predicate logic: interpretation, model, valid formula, consistent formula, inconsistent formula, logical consequence.
3.	Prenex normal form, Skolem theorem, Skolemization algorithm, clausal normal form. 
4.	Theorem of soundness and theorem of completeness for predicate logic; noncontradiction, coherence  and semi-decidability of predicate logic.

Lecture + Seminar  10:
1.	Sequent calculus for predicate logic – rules for quantifiers.
2.	Semantic tableaux method for predicate logic – rules for quantifiers.
3.	Herbrand universe, Herbrand system, Herbrand interpretation, Herbrand theorem; a refutation proof method based on Herbrand theorem (a semi-decidable procedure).

Lecture 11 + Seminar 11:
1.	Substitutions and unifications- theory, algorithm for obtaining the most general unifier o two atoms.
2.	Resolution method in predicate logic. Refinements of resolution. The theorem of soundness and completeness for resolution.
3	Exercises:
•	Compute the most general unifier for two or more atoms.
•	Check if a predicate formula is a theorem / is deductible from a set of formulas using resolution procedure and its refinements.

Lectures 12-14 + Seminars  12-14:
 Boolean algebras, Boolean functions and Logical circuit
	1.  Boolean algebras: definition, properties, principle of duality, examples;
      2.  Boolean functions: definitions, maxterms, minterms, the canonic disjunctive form 
            and the canonic conjunctive form, transformation.
3	Simplification of boolean functions
•	definitions: maximal monoms, central monoms, factorization;
•	Veitch-Karnaugh diagrams method – for functions with 2-3 variables;
•	Quine’s method, Moisil method.
4.  Logical circuits
•	definitions, representations for basic gates (“and”, “or”, “not”) and derived gates (“xor”, “nand”, “nor”) and relations between them.
•	examples of simple logical circuits: “decoder”, ”binary codification” circuit, “comparison circuit”, “addition” circuit;
      5. Exercises:
•	Given a boolean function (with “and”, “or”, “not”, “nor”, “nand” operations): simplification with one of the three methods, implementation of the corresponding logical circuit.
•	Given a logical circuit (with basic and derived gates): write the corresponding boolean function, simplification of this function.
•	Given a boolean function represented using a tableaux containing the values of the function: simplification, implementation of the corresponding logical circuit.

VII. Didactic methods used
•	lecturers, conversations, exercises, individual study;
•	each student, individually, has to solve and present during the seminars, problems from an existing benchmark of proposed problems (M.Lupea, 2006, electronic format), related to the content of the course.	

VIII. Assessment
The examination consists of a written exam with the subject from all the matter (70%).
In the final mark will be considered the activity at the seminars, where some short tests and
individual presentations will be accomplished (30%).

IX. Additional references
1.  W.Bibel: Automated theorem proving, View Verlag, 1987.
2.  Cl.BENZAKEN: Systeme formels. Introduction a la logique, ed.Masson, 1991.
3.   J.P.DELAHAYE: Outils logiques pour l'intelligence artificielle, ed.Eyrolls, 1986.
4.	(ed) A.Thayse: From standard logic to Logic Programming, Ed. J.Wiley, vol1(1989), vol2(1989), vol3(1990). 

	Date,							Course responsible,
       12.04.2007			            		Lect. LUPEA Mihaiela, Ph.D.