UNIVERSITY OF BELGRADE
DEPARTMENT FOR COMPUTER SCIENCE

ARGO

Automated reasoning group



Publications

2024

  1. Salwa Tabet Gonzalez, Predrag Janicic, Julien Narboux: Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving. EPTCS 398, 2024, pp. 21-37
  2. Vesna Marinković, Tijana Šukilović, Filip Marić: Towards Automated Readable Proofs of Ruler and Compass Construction, EPTCS 398, 2024, pp. 11-20

2023

  1. Milan Bankovic, Ivan Drecun, Filip Maric. A proof system for graph (non)-isomorphism verification. Logical Methods in Computer Science. 2023.
  2. Milan Banković. Automation of Triangle Ruler-and-Compass Constructions Using Constraint Solver, presented at ADG 2023.
  3. Vesna Marinković, Tijana Šukilović, Filip Marić. Towards automated readable proofs of ruler and compass constructions, presented at ADG 2023.
  4. Predrag Janicic, Julien Narboux: Automated generation of illustrated proofs in geometry and beyond. Ann. Math. Artif. Intell. 91(6): 797-820 (2023)
  5. Vesna Marinković, Tijana Šukilović, Filip Marić: Automated triangle constructions in hyperbolic geometry, Annals of Mathematics and Artificial Intelligence, vol. 91, pp. 821–849, 2023.
  6. Vesna Marinković: Prolog in Automated Reasoning in Geometry, in book: Prolog: The Next 50 Years, LNAI 13900, pp. 334-345, 2023.

2022

  1. Milan Banković, David Šćepanović.Trail Saving in SMT. Presented at SMT workshop 2022 (part of FLOC 2022).
  2. Predrag Janicic, Julien Narboux: Theorem Proving as Constraint Solving with Coherent Logic. J. Autom. Reason. 66(4): 689-746 (2022)

2021

  1. Milan Banković, Filip Marić. Faradžev Read-type enumeration of non-isomorphic CC systems. Computational Geometry 97 (2021): 101770.
  2. Milan Banković. Automated solving of Sokoban puzzle using artificial intelligence. Presented at YU INFO 2021, Kopaonik, Serbia (in Serbian).
  3. Vesna Marinković. Moderna nastava matematike zasnovana na metodama veštačke inteligencije. Presented at YU INFO 2021, Kopaonik, Serbia (in Serbian).

2020

  1. Mirko Spasić, Milena Vujošević Janičić: Verification supported refactoring of embedded SQL. Software Quality Journal (2020).
  2. Milena Vujošević Janičić: Concurrent Bug Finding Based on Bounded Model Checking. Int. J. Softw. Eng. Knowl. Eng. 30(5): 669-694 (2020)
  3. Milica Selaković, Vesna Marinković, Predrag Janičić: New Dynamics in Dynamic Geometry: Dragging Constructed Points, Journal of Symbolic Computation, Volume 97, March–April 2020, Pages 3-15.
  4. Milena Vujošević Janičić, Filip Marić: Regression verification for automated evaluation of students programs. Comput. Sci. Inf. Syst. 17(1): 205-227 (2020)

2019

  1. Predrag Janičić, Filip Marić, Marko Maliković: Computer-Assisted Proving of Combinatorial Conjectures Over Finite Domains: A Case Study of a Chess Conjecture Logical Methods in Computer Science, Volume 15, Issue 1, 2019, pp. 34:1–34:37
  2. Mladen Nikolić, Vesna Marinković, Zoltan Kovacs, Predrag Janičić: Portfolio Theorem Proving and Prover Runtime Prediction for Geometry, Annals of Mathematics and Artificial Intelligence, Issue 2-4/2019.

2018

  1. Sana Stojanovic Djurdjevic: From informal to formal proofs in Euclidean geometry, Annals of Mathematics and Artificial Intelligence, Issue 85, pp 89-117 [pdf]
  2. Julien Narboux, Predrag Janičić, Jacques Fleuriot: Computer-Assisted Theorem Proving in Synthetic Geometry Handbook of Geometric Constraint Systems Principles (editors Meera Sitharam, Audrey St. John, Jessica Sidman), pp 21-60, Chapman and Hall/CRC, Taylor & Francis Group, 2018.
  3. Milutin Pejović, Mladen Nikolić, Gerard Huevelink, Tomislav Hengl, Milan Kilibarda, Branislav Bajat: Sparse Regression Interaction Models for Spatial Prediction of Soil Properties in 3D, Computers and Geosciences, 2018.
  4. Milutin Pejović, Mladen Nikolić, Branislav Bajat: 3D Soil Texture Mapping with L1 Regularized Multinomial Logistic Regression, 19th Annual Conference of International Association for Mathematical Geosciences (IAMG), 2018.

2017

  1. Dragan Lambić, Mladen Nikolić: Pseudo-Random Number Generator Based on Discrete-Space Chaotic Map, Nonlinear Dynamics, 2017.

2016

  1. Predrag Janičić: Geometrisation of Geometry (invited talk), presented at ADG 2016.
    [pdf]
  2. Vesna Marinković, Mladen Nikolić, Zoltan Kovacs, Predrag Janičić: Portfolio Methods in Theorem Proving for Elementary Geometry, presented at ADG 2016.
    [pdf]
  3. Pascal Schreck, Pascal Mathis, Vesna Marinković, Predrag Janičić: Wernick's List: A Final Update, Forum Geometricorum, vol 16, pp. 69--80, 2016.
    [pdf]
  4. Pascal Schreck, Vesna Marinković, Predrag Janičić, Constructibility Classes for Triangle Location Problems, Mathematics in Computer Science, Springer, vol 10, issue 1, pp. 27--39, 2016.
    [pdf]
  5. Milan Banković: Parallelizing simplex within SMT solvers, Artificial Intelligence Review, accepted for publication, 2016.
    [pdf-draft], [DOI]
  6. Milan Banković: Solving finite-domain linear constraints in presence of the alldifferent, Logical Methods in Computer Science, Vol. 12, issue 3, 2016.
    [pdf-draft], [LMCS]
  7. Milan Banković: Improving SMT solvers using CSP techniques and parallelization techniques. PhD Thesis (Serbian), December 2016.
    [pdf]

2015

  1. Vesna Marinković: On-line Compendium of Triangle Construction Problems with Automatically Generated Solutions, The Teaching of Mathematics, XVIII_1, pp. 29--44, 2015.
    [pdf]
  2. Filip Marić: A Survey of Interactive Theorem Proving, accepted for publication, 2015.
    [pdf]
  3. Filip Marić, Predrag Janičić, Marko Maliković: Proving Correctness of a KRK Chess Endgame Strategy by using Isabelle/HOL and Z3, In 25th International Conference on Automated Deduction - CADE 25, Volume 9195 of the series Lecture Notes in Computer Science, pp 256-271.
    [pdf]
  4. Vesna Marinković, Predrag Janičić, Pascal Schreck: Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems, In F. Botana and P. Quaresma, editors, Automated Deduction in Geometry, ADG 2014, volume 9201 of Lecture Notes in Computer Science, pp. 72--93. Springer, 2015.
    [pdf]
  5. Vesna Marinković: ArgoTriCS - Automated Triangle Construction Solver, Journal of Experimental & Theoretical Artificial Intelligence, accepted for publication
    [pdf-draft]
  6. Vesna Marinković: Automated Solving of Construction Problems in Geometry. PhD Thesis (Serbian), June 2015.
    [pdf]
  7. Milan Banković: Extending SMT solvers with support for finite domain alldifferent constraint, Constraints, accepted for publication, 2015
    [pdf-draft], [DOI]

2014

  1. Sana Stojanovic Djurdjevic, Julien Narboux, Predrag Janicic: Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry, Annals of Mathematics and Artificial Intelligence, accepted for publication [pdf]
  2. Milena Vujošević Janičić: System LAV and Automated Evaluation of Students’ Programs, Dagstuhl Reports, Volume 4, Issue 8, 2014.
    [pdf]
  3. Filip Marić, Danijela Petrović: Formalizing Complex Plane Geometry. Annals of Mathematics and Artificial Intelligence, Springer, accepted, 2014.
    4. [pdf]
  4. Mirko Stojadinović: Air Traffic Controller Shift Scheduling by Reduction to CSP, SAT and SAT-related Problems, CP 2014, 8656, 2014.
  5. Mirko Stojadinović, Filip Marić: meSAT: Multiple Encodings of CSP to SAT, Constraints, 19(4), 2014. [pdf-draft]
  6. Jelena Slivka, Mladen Nikolić, Kosta Ristovski, Vladan Radosavljević, Zoran Obradović: Distributed Gaussian Conditional Random Fields Based Regression for Large Evolving Graphs, SIAM International Conference on Data Mining, Workshop on Mining Networks and Graphs, 2014.
  7. Sana Stojanović, Julien Narboux, Marc Bezem, Predrag Janičić: A Vernacular for Coherent Logic, Intelligent Computer Mathematics - CICM 2014, Lecture Notes in Computer Science, Volume 8543, Springer [pdf]
  8. Vesna Marinković, Predrag Janičić, Pascal Schreck: Solving Geometric Construction Problems Supported by Theorem Proving, presented at ADG 2014.
    [pdf]
  9. Vesna Marinković: Proof Simplification in the Framework of Coherent Logic, Computing and Informatics, vol 34, no. 02, pp. 337--366, 2015.
    [pdf-draft]

2013

  1. Mladen Nikolić: Guiding Search in Automathed Theorem Proving. PhD Thesis (Serbian), May 2013. [pdf]
  2. Marko Maliković, Predrag Janičić: Proving Correctness of a KRK Chess Endgame Strategy by SAT-based Constraint Solving. ICGA Journal (International Computer Games Association), June 2013. [pdf-draft]
  3. Milena Vujošević-Janičić, Mladen Nikolić, Dušan Tošić, Viktor Kuncak: Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments. Information and Software Technology, Elsevier 2013. [ DOI ]
  4. Sana Stojanović: Preprocessing of the Axiomatic System for More Efficient Automated Proving and Shorter Proofs. Automated Deduction in Geometry, Lecture Notes in Computer Science, Volume 7993, Springer
    5. [pdf]
  5. Mladen Nikolić, Filip Marić, Predrag Janičić: Simple Algorithm Portfolio for SAT, Artificial Intelligence Review, Volume 40, Issue 4, 2013.
    [pdf]

2012

  1. Predrag Janičić: Uniform Reduction to SAT. Logical Methods in Computer Science, Volume 8, Issue 3, Paper 30, 2012.
  2. Tomislav Hengl, Mladen Nikolić, Robert MacMillan: Mapping Efficiency and Information Content. International Journal of Applied Earth Observation and Geoinformation, 2012. [DOI]
  3. Mirko Spasić, Filip Marić: Formalization of Incremental Simplex Algorithm by Stepwise Refinement. In FM2012 - 18th International Symposium on Formal Methods, LNCS 7436, Springer, 2012.
    4. [pdf] [slides]
  4. Danijela Petrović, Filip Marić: Formalizing Analytic Geometries. Presented at ADG2012 - Automated Deductinon in Geometry, Edinburgh, UK, 2012.
  5. Mladen Nikolić, Predrag Janičić: CDCL-Based Abstract State Transition System for Coherent Logic. In J. Jeuring et al. (Eds.): Intelligent Computer Mathematics, (CICM 2012), LNAI 7362, pp. 263–278, 2012.
    [pdf]
  6. Vesna Marinković, Predrag Janičić: Towards Understanding Triangle Construction Problems. In J. Jeuring et al. (Eds.): Intelligent Computer Mathematics, (CICM 2012), LNAI 7362, pp. 126–141, 2012.
    [pdf]
  7. Filip Marić, Miodrag Živković, Bojan Vučković: Formalizing Frankl's Conjecture: FC-families. In J. Jeuring et al. (Eds.): Intelligent Computer Mathematics (CICM 2012). Calculemus track. LNAI 7362, 2012.
    [pdf]
  8. Filip Marić, Ivan Petrović, Danijela Petrović, Predrag Janičić: Formalization and Implementation of Algebraic Methods in Geometry. In Pedro Quaresma and Ralph-Johan Back: Proceedings First Workshop on CTP Components for Educational Software (THedu'11), Wrocław, Poland, 31th July 2011, Electronic Proceedings in Theoretical Computer Science 79, pp. 63–81.
  9. Milena Vujošević-Janičić, Viktor Kuncak: Development and Evaluation of LAV: an SMT-Based Error Finding Platform. Verified Software: Theories, Tools, Experiments. Lecture Notes in Computer Science, Volume 7152, Springer 2012, ISBN 978-3-642-27704-7.
    [pdf] [slides]
  10. Milan Banković: ArgoSMTExpression: an SMT-LIB 2.0 compliant expression library, presented at Pragmatics of SAT 2012.
    [pdf] [slides]
  11. Mladen Nikolić: Measuring Similarity of Graph Nodes by Neighbor Matching, Intelligent Data Analysis, Volume 40, Issue 4, 2012.
    [pdf]

2011

  1. Sana Stojanović, Vesna Pavlović, Predrag Janičić: A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs. Automated Deduction in Geometry, Lecture Notes in Computer Science, Volume 6877, Springer. [pdf]
  2. Predrag Janičić: Automated Reasoning: Some Successes and New Challenge, Proceedings of 22nd Central European Conference on Information and Intelligent Systems, CECiiS 2011 (Invited lecture), 2011.
    [pdf]
  3. Predrag Janičić, Julien Narboux, Pedro Quaresma: The Area Method: A Recapitulation. Journal of Automated Reasoning, to appear. [pdf]
  4. Filip Marić, Predrag Janičić: Formalization of Abstract State Transition Systems for SAT, Logical Methods in Computer Science, 7(3), 2011.
    [pdf]

2010

  1. Filip Marić: Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle/HOL, Theoretical Computer Science, Volume 411, Number 50, 2010.
    [pdf]
  2. Predrag Janičić: Geometry Construction Language, Journal of Automated Reasoning, Volume 44, Issue 1-2, 2010.
    [pdf]
  3. Filip Marić, Predrag Janičić: Formal Correctness Proof for DPLL Procedure, Informatica, Volume 21, Number 1, 57-78, 2010
    [pdf]
  4. Mladen Nikolić: Statistical Methodology for Comparison of SAT Solvers, In Theory and Applications of Satisfiability Testing - SAT 2010, LNCS 6175, pp. 209--222, Springer, 2010.
    [pdf] [slides]
  5. Filip Marić, Predrag Janičić: URBiVA: Uniform Reduction to Bit-Vector Arithmetic, presented at IJCAR 2010.
    [pdf] [slides]
  6. Sana Stojanović, Vesna Pavlović, Predrag Janičić: Automated Generation of Formal and Readable Proofs in Geometry Using Coherent Logic, presented at ADG 2010.
    [pdf] [slides]
  7. Milan Banković, Filip Marić: An Alldifferent Constraint Solver in SMT, presented at SMT Workshop 2010.
    [pdf] [slides]

2009

  1. Mladen Nikolić, Filip Marić, Predrag Janičić: Instance Based Selection of Policies for SAT Solvers, In Theory and Applications of Satisfiability Testing, LNCS 5584, pp. 326--340, Springer, 2009.
    [pdf]
  2. Filip Marić: Formalization and Implementation of Modern SAT Solvers, Journal of Automated Reasoning 43(1), pp.~81--119, Springer, 2009.
    [pdf]
  3. Filip Marić, Predrag Janičić: SAT Verification project, TPHOLs 2009, Emerging trends, pp. 40-49.
    [pdf]
  4. Filip Marić: Formalization, Implementation and Verification of SAT solvers. PhD Thesis (Serbian), june 2009.
    [pdf]

2008

  1. Mladen Nikolić. Methodolgy for choosing suitable values of parameters of SAT solvers. Master Thesis (Serbian), December 2008.
    [pdf]
  2. Pedro Quaresma, Predrag Janičić, Jelena Tomašević, Milena Vujošević Janičić, Dušan Tošić. XML-based Format for Geometry --- XML-based Format for Descriptions of Geometrical Constructions and Geometrical Proofs. Chapter in Communicating Mathematics in Digital Era, edited by. J. M. Borwein, E. M. Rocha and J. F. Rodrigues, Pages 183 -- 197, 2008.
    [pdf]
  3. Jelena Tomašević. XML databases and their applications in lexical resources management. Master Thesis, September 2008.
    [pdf]
  4. Milena Vujošević-Janičić. Ensuring Safe Usage of Buffers in Programming Language C. In Proceedings of ICSOFT 2008 --- Third International Conference on Software and Data Technologies, Volume PL/DPS/KE, Pages 29 -- 36, 2008.
    [pdf] [slides]
  5. Milena Vujošević-Janičić. Automated Detection of Buffer Overflows in Programming Language C. Master Thesis, June 2008.
    [pdf]
  6. Milena Vujošvić-Janičić, Filip Marić, Dušan Tošić. Using Simplex Method in Verifying Software Safety. In Proceedings of BALCOR 2007 --- Eight Balkan Conference on Operetional Research, Pages 305 -- 319, 2008.
    [pdf]

2007

  1. Predrag Janičić, Pedro Quaresma. Automated Verification of Regular Constructions. Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence, Springer-Verlag, Volume 4869, 2007.
  2. Predrag Janičić, Alan Bundy. Automatic synthesis of decision procedures. Calculemus, Springer, Lecture Notes in Artificial Intelligence, Volume 4573, Pages 80 -- 93, 2007.
    [short-pdf] [ long-pdf] [code] [slides]
  3. Pedro Quaresma, Predrag Janičić. 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, Pages 35 -- 48, 15 May 2007.
  4. Andrija Tomović, Predrag Janičić. A Variant of N-gram-based Classification of Languages, AI*IA, Lecture Notes in Artificial Intelligence, Volume 4733, Pages 410 -- 421, 2007.
  5. Milena Vujošević-Janičić, Jelena Tomašević, Predrag Janičić. Random k-GD-SAT Model and its Phase Transition. Journal of Universal Computer Science, Volume 13, Issue 4, Pages 572 -- 591, 2007.

2006

  1. Predrag Janičić. 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, Springer-Verlag, Volume 4151, Pages 58 -- 73, 2006.
    [pdf] [slides]
  2. Predrag Janičić, Pedro Quaresma. System Description: GCLCprover + GeoThms. International Joint Conference on Automated Reasoning (IJCAR-2006), Furbach, Ulrich and Shankar, Natarajan, editors. Springer-Verlag, Lecture Notes in Artificial Intelligence, Volume 4130, Pages 145 -- 150, 2006.
    [pdf]
  3. Predrag Janičić, Pedro Quaresma. Automatic Verification of Regular Constructions in Dynamic Geometry Systems, Automated Deduction in Geometry, Pages 39 -- 51, 2006.
  4. Petar Maksimović, Predrag Janičić. Simple characterization of functionally complete one-element sets of propositional connectives. Mathematical Logic Quarterly, 52(5), Pages 498 -- 504, 2006.
  5. Miroslav Marić, Sana Stojanović. Adaptation of Edges in a Triangular Mesh. SISY 2006 --- 4th Serbian-Hungarian Joint Symposium on Intelligent Systems, 2006.
    [pdf]
  6. Pedro Quaresma, Predrag Janičić. Integrating Dynamic Geometry SoftwareDeduction Systems, and Theorem Repositories, Mathematical Knowledge Management (MKM-2006), Borwein, J.M. and Farmer, W.M, editors. Lecture Notes in Artificial Intelligence, Volume 4108, Springer-Verlag, Pages 280 -- 294, 2006.
    [pdf]
  7. Andrija Tomović, Predrag Janičić, Vlado Kešelj. N-gram-based Classification and Unsupervised Hierarchical Clustering of Genome Sequences, Computer Methods and Programs in Biomedicine, Elsevier, Volume 8, Issue 2, Pages 137 -- 153, 2006.
    [pdf]

2005

  1. Dejan Jovanović, Predrag Janičić. Logical Analysis of Hash Functions. Frontiers of Combining Systems (FroCoS), Springer, Lecture Notes in Artificial Intelligence, Volume 3717, Pages 200 -- 215, 2005.
    [pdf] [slides]

2004

  1. Mirjana Đorić, Predrag Janičić. Constructions, Instructions, Interactions, Teaching Mathematics and its Applications. Oxford University Press, Volume 23, Issue 2, Pages 69 -- 88, 2004.
    [pdf]
  2. Filip Marić, Borovčanin Momčilo, Miroslav Marić. Quantifier elimination in fields. ETRAN, 2004.
    [pdf]
  3. Filip Marić, Predrag Janičić. SMT-LIB in XML clothes. Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2004), Dublin, July 2004.
    [short-pdf] [long-pdf]
  4. Filip Marić, Predrag Janičić. ARGO-LIB: A Generic Platform for Decision Procedures. IJCAR-04, Springer, Lecture Notes in Artificial Intelligence, Volume 3097, Pages 213 -- 217, 2004.
    [pdf]