Predrag Janicic

I was born in December of 1968 in the city of Pristina, Serbia, Yugoslavia where I graduated from “Miladin Popovic” High School in 1987. After a year of obligatory Army service, in October of 1988 I enrolled the University of Belgrade, Faculty of Mathematics, Department of Computer Science. I graduated from University in 1993. My GPA (grade point average) was highest possible (10.00). The same year I was offered position of a Teaching Assistant. During 1996, 2001, and 2002 I worked eight months as a visiting researcher at prof. Alan Bundy's Mathematical Reasoning Group (School of Informatics, University of Edinburgh). In 1996 I received my MSc degree and in 2001 my PhD degree in Computer Science from the Faculty of Mathematics, University of Belgrade. Since May 2008, I have a position of associate professor and presently teach courses Programming, Computer Graphics, and Artificial Intelligence. My research interests are in the field of Automated Reasoning and I lead the ARGO group. I am a member of Association for Automated Reasoning. Over the past several years I did a number of research software projects and software projects for industrial applications. In my spare time I enjoy arts.

Awards & Distinctions

During my high school I took part in a number of national and international competitions in mathematics and physics. In 1987 I won the 1st place in Yugoslav Federal Competition in Mathematics, the 2nd prize in Balkan Mathematical Olympiad and I participated in International Mathematical Olympiad. I was awarded as the best student of the generation at the University of Belgrade. During my studies I was recipient of numerous other awards.

Curriculum Vitae

English
Serbian

Education and Degrees

BSc: June 1993

1988-1993 Department of Computer Science, Faculty of Mathematics, University of Belgrade. Graduated in June 1993 with GPA (grade point average) 10.00 (out of 10.00). Final thesis: "Acting of Isometry Groups on Hyperbolical Plane"; advisor prof. Z.Lucic (Univ. of Belgrade)

MSc: July 1996

1993-1996 Master of Science degree from Department of Computer Science, Faculty of Mathematics, University of Belgrade. GPA 10.00; Master's thesis: "One Method for Automated Geometry Theorems Proving"; advisor: prof. Z.Lucic (Univ. of Belgrade). The thesis in Serbian: “Jedan metod za automatsko dokazivanje teorema geometrije”.

PhD: January 2001

1996-2000 Doctor of Philosophy in Computer Science, Department of Computer Science Department, Faculty of Mathematics, University of Belgrade. PhD thesis: "Building decision procedures into theorem provers”; advisors: prof. A.Bundy (Univ. of Edinburgh) and prof. Z.Mijajlovic (Univ. of Belgrade). The thesis in Serbian (with summaries in English for all chapters): "Ugradnja procedura odlucivanja u sisteme za automatsko rezonovanje".

Collaborations and Cooperations

Visits

During 1996, 2001, and 2002 I worked eight months as a visiting researcher at prof. Alan Bundy's Mathematical Reasoning Group (School of Informatics, University of Edinburgh).

I also visited several other universities and gave lectures at the University of Edinburgh (1996, 2001, 2002), University of Birmingham (2001), University of Cambridge (2002), Heriot-Watt University (Edinburgh) (2002), Technical University Berlin (2002), University of Genoa (2003), Technical University Dresden (2004), University of Coimbra (2005).

Co-Authors and Collaborators

I am happy and proud that I have worked and work with the following people:

Alan Bundy

Nenad Dedic

Mirjana Djoric

Ian Green

Mateja Jamnik

Dejan Jovanovic

Vlado Keselj

Stevan Kordic

Filip Maric

Goran Nenadic

Aleksandar Samardzic

Irena Spasic

Goran Terzic

Andrija Tomovic

Pedro Quaresma

Industrial Cooperation

Over the last years I had a number of collaborations with industry, mostly in domains of AI (Artificial Intelligence) systems, cryptography, data bases etc.

News and Miscellaneous

Announcements

A new edition of my textbook "Mathematical Logic in Computer Science" has been released in May 2009.

Future Conferences and Meetings

NEW! FM2009, 16th International Symposium on Formal Methods, Eindhoven, the Netherlands, October 30 - November 7, 2009

Other Interests

In my spare time I enjoy arts.

Personal Information

Favorite Links

Professional Activities

Editorial Responsibilities / Refereeing

I have been doing refereeing for the journals "Journal of Automated Reasoning", "Theoretical Computer Science", "Information and Computation" and for the conferences "International Joint Conference on Automated Reasoning" (IJCAR), "Pragmatics of Decision Procedures in Automated Reasoning" (PDPAR), Frontiers in Combining Systems (FroCoS).

I am a member of the Editorial Board of the journal Transactions on Advanced Research.

Professional Societies /Administrative Service

I am a member of Association for Automated Reasoning.

Congress and Workshop Organization

I served as a member of the Programme Committee for:

Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '03) (Miami 2003)

Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05) (Edinburgh, 2005),

CADGME 2009 Working Group Convergence on Mathematics Assistants, Linz, July 11-13, 2009.

PLLMS 2009 Workshop on Programming Languages for Mechanized Mathematics Systems, Munich, Germany, August 21, 2009.

FM2009, 16th International Symposium on Formal Methods, Eindhoven, the Netherlands, October 30 - November 7, 2009

Other Services, Duties, and Functions

I served two mandates as a member of the Council of the Faculty of Mathematics.

Research

Research Areas and Applications

My research interests are in automated reasoning and in mathematical software. Especially, I am interested in the problem of the combining and integrating decision procedures into heuristic theorem provers and in the phenomenon of phase transition in NP complete problems. I am also interested in automated theorem proving in geometry. I lead the ARGO group, engaged in these research topics.

Other Scientific Interests

I am interested in computational geometry, in visualization of geometry and in links between geometry and computer science.

Publications

Here is the list of my publications.

Research Projects / Grants

In 1996, I was awarded a fellowship from the British Scholarship Trust. Under this grant I spent three months during 1996 at School of Informatics, University of Edinburgh.

In 2001, together with prof. Alan Bundy (School of Informatics, University of Edinburgh) I was awarded EPSRC research grant GR/R52954/01 "Flexible incorporation of decision procedures into the LambdaClam proof-planning system". Under this grant I spent five months during 2001 and 2002 at School of Informatics, University of Edinburgh.

In 2005, by Coimbra Group Hospitality Scheme and partially by the programme POSC, by the Centro International de Matemática (CIM), I was awarded a grant to spend one month as a visiting researcher in the University of Coimbra.

I was involved in research projects 1379 and 1646 supported by the Ministry of Science of the Republic of Serbia.

Since 2006, I am the leader of the research project 144030 supported by the Ministry of Science of the Republic of Serbia.

Software

Over the past several years I did a number of research software projects. Here it can be downloaded some of the software that I wrote.

Talks / Presentations

Here is the list of my seminar and conference talks.

Selected Papers/Publications/Books (in reversed chronological order)

Publications

Automated reasoning

Predrag Janicic: Geometry Constructions Language. Journal of Automated Reasoning, Volume 44, Issue 1-2, 2010.

Filip Maric, Predrag Janicic: Formal Correctness Proof for DPLL Procedure. Informatica, Volume 21, Number 1, 57-78, 2010.

Mladen Nikolic, Filip Maric, Predrag Janicic: Instance Based Selection of Policies for SAT Solvers. Theory and Applications of Satisfiability Testing 2009, Lecture Notes in Computer Science, Volume 5584. pages 326-340, 2009. Springer.

Predrag Janicic, Pedro Quaresma: Automated Verification of Regular Constructions, Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence, volume 4869, Springer-Verlag, 2007.

Predrag Janicic, Alan Bundy: Automatic synthesis of decision procedures, Calculemus 2007. Lecture Notes in Artificial Intelligence, volume 4573, pages 80-93, Springer. Longer version, corresponding PROLOG code.

Milena Vujosevic-Janicic, Jelena Tomasevic, Predrag Janicic: Random k-GD-Sat Model and its Phase Transition, Journal of Universal Computer Science, Vol. 13, No. 4, pp. 572-591. 2007.

Petar Maksimovic, Predrag Janicic: Simple characterization of functionally complete one-element sets of propositional connectives, Mathematical Logic Quarterly, 52(5), pp 498--504, 2006.

Predrag Janicic, Pedro Quaresma: System Description: GCLCprover + GeoThms, International Joint Conference on Automated Reasoning (IJCAR-2006), Furbach, Ulrich and Shankar, Natarajan, editors. Lecture Notes in Artificial Intelligence, volume 4130, pages 145-150, Springer-Verlag, 2006. Draft version available.

Dejan Jovanovic, Predrag Janicic: Logical Analysis of Hash Functions, Frontiers of Combining Systems (FroCoS), Lecture Notes in Artificial Intelligence, volume 3717, pages 200-215, Springer, 2005.

Filip Maric, Predrag Janicic: SMT-LIB in XML clothes, Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2004), Dublin, July 2004. Longer version also available.

Filip Maric, Predrag Janicic: ARGO-LIB: A Generic Platform for Decision Procedures, IJCAR-04, Lecture Notes in Artificial Intelligence, volume 3097, pages 213-217, Springer, 2004. Copyright Springer

Mateja Jamnik, Predrag Janicic: Learning Strategies for Mechanised Building of Decision Procedures, Electronic Notes in Theoretical Computer Science, Elsevier, Volume 86, number 1, 2003.

Mateja Jamnik, Predrag Janicic: Can decision procedures be automatically learnt?, Proceedings of the 4th International Workshop on First order Theorem Proving (FTP'03). Valencia, Spain, June 12-14, 2003.

Predrag Janicic, Alan Bundy: A General Setting for Combining and Augmenting Decision Procedures into Theorem Provers, Journal of Automated Reasoning Vol. 28 No. 3, pp 257-305, 2002. Copyright Kluwer Academic Publisher. Draft version available. (Also available as EDI-INF-RR-0095, Division of Informatics, University of Edinburgh)

Predrag Janicic, Nenad Dedic, Goran Terzic: On different models for generating SAT problems, Computing and Informatics Volume 20, Number 5, pp 451-469, 2001. Draft version available.

Predrag Janicic, Alan Bundy: Strict General Setting for Building-in Decision Procedures into Theorem Provers, Proceedings of the first International Joint Conference on Automated Reasoning (IJCAR '01), Siena, Italy, June 18-23, 2001. Longer version available. (Also available as EDI-INF-RR-0097, Division of Informatics, University of Edinburgh)

Predrag Janicic: GD-SAT model and crossover line, Journal of Theoretical and Experimental Artificial Intelligence, Vol 13, Number 13, pp 181-198, 2001. Copyright Taylor & Francis. Draft version available.

Predrag Janicic, Alan Bundy, Ian Green: A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers , CADE-16, Lecture Notes in Artificial Intelligence 1632, pp: 127-141, Springer, 1999. Copyright Springer. (Also available as EDI-INF-RR-0096, Division of Informatics, University of Edinburgh)

Predrag Janicic, Ian Green, Alan Bundy: A Comparison of Decision Procedures in Presburger Arithmetic, Proceedings of VIII International Conference on Logic and Computer Science (LIRA '97) pp: 91-101, Novi Sad, September 01-04, 1997. (also available as Research Paper 872, Department of AI, University of Edinburgh)

Predrag Janicic, Stevan Kordic: EUCLID - the Geometry Theorem Prover, FILOMAT, Nis, 9:3 (1995), 723-732

Geometry, visualization, mathematical software

Pedro Quaresma, Predrag Janicic, Jelena Tomasevic, Milena Vujosevic-Janicic, Dusan Tosic: XML-based Format for Geometry --- XML-based Format for Descriptions of Geometrical Constructions and Geometrical Proofs. Chapter in Communicating Mathematics in Digital Era (Eds J. M. Borwein, E. M. Rocha and J. F. Rodrigues), pages 183--197. A K Peters, Ltd. Wellesley, MA, USA, 2008.

Pedro Quaresma, Predrag Janicic: GeoThms — a Web System for Euclidean Constructive Geometry, Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006), Electronic Notes in Theoretical Computer Science, Volume 174, Issue 2, 15 May 2007, Pages 35-48, Elsevier

Predrag Janicic: GCLC -- A Tool for Constructive Euclidean Geometry and More than That, International Congress of Mathematical Software (ICMS 2006), Takayama, Nobuki and Iglesias, Andres and Gutierrez, Jaime, editors. Lecture Notes in Computer Science, volume 4151, pages 58-73, Springer-Verlag, 2006. Draft version available.

Pedro Quaresma, Predrag Janicic: Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories, Mathematical Knowledge Management (MKM-2006), Borwein, J.M. and Farmer, W.M, editors. Lecture Notes in Artificial Intelligence, volume 4108, pages 280-294, Springer-Verlag, 2006. Draft version available.

Mirjana Djoric, Predrag Janicic: Constructions, Instructions, Interactions, Teaching Mathematics and its Applications, Oxford University Press, Volume 23, Issue 2, pp 69-88, 2004. Draft version available.

Predrag Janicic, Ivan Trajkovic: WinGCLC --- a Workbench for Formally Describing Figures, Proceedings of the Spring Conference on Computer Graphics (SCCG 2003), April, 24-26, 2003, ACM Press, New York, USA

Data mining

Andrija Tomovic, Predrag Janicic: A Variant of N-gram-based Classification of Languages, AI*IA, Lecture Notes in Artificial Intelligence, volume 4733, 2007.

Andrija Tomovic, Predrag Janicic, Vlado Keselj: N-gram-based Classification and Unsupervised Hierarchical Clustering of Genome Sequences, Computer Methods and Programs in Biomedicine, Elsevier, volume 8, issue 2, 2006, pp137-153. Draft version available.

Selected unpublished papers and notes

Predrag Janicic, Alan Bundy: Implementation of GS framework within LambdaClam proof planning system, 2004.

Learning Stochastic Unambiguous Context-Free Grammars 1999.

Programiranje logickih igara i sistem GAME-MAKER 1995. ("Computer Game Playing and the GAME-MAKER system"); in Serbian only.

Zasnivanje euklidske geometrije 1994. ("Formal Foundations of Euclidian Geometry"); in Serbian only.

Books

Predrag Janicic: Matematicka logika u racunarstvu, Beograd ("Mathematical Logic for Computer Science"); in Serbian only.

Goran Nenadic, Predrag Janicic, Aleksandar Samardzic: LaTeX za autore, Beograd, Kompjuter biblioteka, 2003. ("LaTeX for authors"); in Serbian only. Primeri iz knjige i Vodic za LaTeX2e

Irena Spasic, Predrag Janicic: Teorija algoritama, jezika i automata – zbirka zadataka, Matematicki fakultet, Beograd, 2000 (“Theory of algorithms, languages and automata – collection of problems”); in Serbian only.

Predrag Janicic: Zbirka zadataka iz geometrije, Skripta internacional, Beograd, 1997. (2nd edition 1998, 3rd edition 1999, 4th edition 2003) ("Collection of problems in geometry"); in Serbian only.

Predrag Janicic, Goran Nenadic: Osnovi LaTeX-a, VEDES, Beograd, 1995. ("Fundamentals of LaTeX"); in Serbian only.

Software

HIP ((c) 1990,1993; A program on acting of isometric groups on a hyperbolical plane; runs under MS DOS)

PENTOMINO ((c) 1993; A program for the intellect game of Pentomino; runs under MS DOS)

REVERSI ((c) 1994; A program for the game of Reversi/Othello; runs under MS DOS)

EUCLID ((c) 1992,1996; Geometry Theorems Prover; runs under MS DOS)

GCLC 8.0, WinGCLC 2008 ((c) 1996-2008); A tool for producing mathematical digital illustrations (in LaTeX and bitmap format) and for teaching geometry)

Implementation of the GS framework for the LambdaClam proof planning system (Copyright (c) 2001, 2002; written in PROLOG and (Teyjus) LambdaPROLOG, runs under UNIX; work supported by EPSRC grant GR/R52954/01)

Teaching

Current and Future Teaching

In 2006/07 I teach the following courses: Programming 1, and Programming 2.

Courses taught

Over the previous years, I taught the following courses: Mathematical Logic in Computer Science, Computer Graphics. Also, I worked as a teaching assistant for the courses in Foundations of geometry, Theory of algorithms, languages and automata, Applications of computers (Algorithmics). I taught several post-graduate courses, including Theoretical computer science and Automated reasoning..

Teaching and Course Materials

Here are some materials for these courses (in Serbian only).

Materijali za kurseve Programiranje 1 i 2, Osnovi geometrije, Teorija algoritama, jezika i automata, Primene racunara (Algoritmika), Matematicka logika u racunarstvu, Racunarska grafika, Teorijsko racunarstvo (samo na srpskom jeziku):

Programiranje 1 i 2 (1. godina/I smer)

Osnovi geometrije (2. godina/svi smerovi)
Ispitni rokovi (do 2002 godine), skripte, spiskovi, veliki zadatak

Zbirka zadataka iz geometrije (11.01.2007)

Teorija algoritama, jezika i automata (3. godina/R smer)
Ispitni rokovi (april 1992 - mart 2003)
Spiskovi i statistika (novembar 1997 - mart 2003)

Primene racunara (4. godina/R smer)
Ispitni rokovi (od 1994/95 do 2000/01: jun 1995 - maj 2002)
Spiskovi i statistika (od 1994/95 do 2000/01: jun 1995 - maj 2002)
Materijali za vezbe
Ratna skripta (1999)

Matematicka logika u racunarstvu (4. godina/R smer)

Racunarska grafika (4. godina/R smer ; 3. godina/I smer)
Skripta (2007/08)
Rezultati ispita (2009/10)
Slajdovi za predavanja
Ispitna pitanja
Materijali za kurs "Racunarska grafika" sa Univerziteta u Novom Sadu, autor dr Dragan Masulovic

Vestacka inteligencija (3. godina/I smer)
Skripta (2008/09)
Rezultati testova i ispita (2009/10)

Poslediplomske studije -- pregled oblasti i tema

Prethodni ispitni rokovi i rezultati

This page is always under construction, but is never up-to-date.

This page is structured following the guidelines provided by The International Mathematical Union (IMU) and the lines of the Mathematician's Professional Homepage (MPH).