Automated Reasoning Group

Our international research group brings together people from various departments and universities who are interested in computational logic. Our research activities focus on different aspects of computational logic, namely automated theorem proving, interactive theorem proving and working with large formal (mainly mathematical) knowledge bases (KBs). We are also interested in typing, model checking and declarative and functional programming.

Our tools for automated reasoning over such KBs MaLARea and SINe have won two categories in the world automated reasoning championship (CADE) in 2008, and the first two places in the commercially sponsored SUMO Reasoning Prize in 2008. Our future plans include further novel combinations of inductive (e.g., machine learning) and deductive (e.g., automated theorem proving) reasoning.

Motto

Logic-based computer science is the most exciting field of our times. (Bruno Buchberger)

People

Petr Štěpánek

prof. RNDr. Petr Štěpánek, DrSc.

department: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
e-mail: Petr.Stepanek (at) mff.cuni.cz
www: http://kti.mff.cuni.cz/~stepanek/
research areas: Formal methods, declarative programming, logic
DBLP
Josef Urban

Mgr. Josef Urban, Ph.D.

department: Foundations Group of ICIS, Radboud University in Nijmegen
e-mail: Josef.Urban (at) gmail.com
www: http://cs.ru.nl/~urban/
research areas: Automated Reasoning, inductive reasoning, formalization and computer-verification of mathematics
DBLP
Jiří Vyskočil

RNDr. Jiří Vyskočil, Ph.D.

department: Department of Cybernetics, Czech Technical University in Prague
e-mail: jiri.vyskocil (at) gmail.com
www: http://labe.felk.cvut.cz/~vyskocil/
research areas: Automated Reasoning
DBLP
Petr Pudlák

RNDr. Petr Pudlák, Ph.D.

e-mail: petr (at) pudlak.name
www: http://petr.pudlak.name
research areas: Automated theorem proving, functional programs, logic systems, Semantic Web
DBLP
David Stanovský

RNDr. David Stanovský, Ph.D.

department: Department of Algebra, Charles University in Prague
e-mail: stanovsk (at) karlin.mff.cuni.cz
www: http://www.karlin.mff.cuni.cz/~stanovsk/
research areas: General algebra, automated theorem proving
DBLP
Ondřej Kunčar

Mgr. Ondřej Kunčar

department: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
e-mail: ondrej.kuncar (at) mff.cuni.cz
www: http://ktiml.mff.cuni.cz/~kuncar/
research areas: Computational logic, interactive theorem provers, systems for formal mathematics
Vladimír Šišma

Mgr. Vladimír Šišma

department: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
e-mail: vsisma (at) sidaaq.cz
research areas: Automated reasoning
Martin Suda

RNDr. Martin Suda

department: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague, and Research Group of Automation of Logic, Max-Planck-Institut für Informatik in Saarbrücken
e-mail: martin.suda (at) gmail.com
www: http://ktiml.ms.mff.cuni.cz/~suda/
research areas: Automated theorem proving, accessing external functions from prover loop
DBLP
Filip Děchtěrenko

Bc. Filip Děchtěrenko

department: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
e-mail: filip.dechterenko (at) gmail.com
research areas: Automated theorem proving

Alumni

  • Jan Hrůza
  • Jan Jakubuv
  • Jiří Vyskočil
  • Josef Urban
  • Josef Hynek
  • Kryštof Hoder
  • Mikoláš Janota
  • Pavel Vanoušek
  • Petr Pudlák
  • Roman Barták
  • Zdeněk Hellriegel

Selected Publications

  • Proving Valid Quantified Boolean Formulas in HOL Light.
    Ondřej Kunčar. ITP 2011 (accepted).
  • MaLeCoP: Machine Learning Connection Prover.
    Josef Urban, Jiří Vyskočil, Petr Štěpánek. TABLEAUX 2011 (accepted).
  • Automated theorem proving in quasigroup and loop theory.
    J. D. Phillips, David Stanovský. AI Commun. 23(2-3): 267-283 (2010)
  • Evaluation of Automated Theorem Proving on the Mizar Mathematical Library.
    Josef Urban, Kryštof Hoder, Andrei Voronkov. ICMS 2010: 155-166
  • On the Saturation of YAGO.
    Martin Suda, Christoph Weidenbach, Patrick Wischnewski. IJCAR 2010: 441-456
  • Automated Proof Compression by Invention of New Definitions.
    Jiří Vyskočil, David Stanovský, Josef Urban. LPAR (Dakar) 2010: 447-462
  • A Wiki for Mizar: Motivation, Considerations, and Initial Prototype.
    Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers. AISC/MKM/Calculemus 2010: 455-469
  • Solving the $100 modal logic challenge.
    Florian Rabe, Petr Pudlák, Geoff Sutcliffe, Weina Shen. J. Applied Logic 7(1): 113-130 (2009)
  • External Sources of Axioms in Automated Theorem Proving.
    Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo. KI 2009: 281-288
  • MaLARea SG1-Machine Learner for Automated Reasoning with Semantic Guidance.
    Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jiří Vyskočil. IJCAR 2008: 441-456
  • ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments.
    Josef Urban, Geoff Sutcliffe. Mathematics in Computer Science 2(2): 231-251 (2008)
  • Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics.
    Josef Urban. International Journal on Artificial Intelligence Tools 15(1): 109-130 (2006)
  • MPTP 0.2: Design, Implementation, and Initial Experiments.
    Josef Urban. J. Autom. Reasoning 37(1-2): 21-43 (2006)
  • MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics.
    Josef Urban. J. Applied Logic 4(4): 414-427 (2006)
  • Transformations of Logic Programs.
    Olga Štěpánková, Petr Štěpánek. J. Logic Programming 1(4): 305-318 (1984)
  • Horn Clause Programs for Recursive Functions.
    Jan Šebelík, Petr Štěpánek. Logic Programming, K. L. Clark, S.-Å. Tärnlund (editors). Academic Press (1982)

Research

  • Automated reasoning - is an area of computer science dedicated to understanding different aspects of reasoning in a way that allows the creation of software which allows computers to reason completely or nearly completely, automatically
  • Automated theorem proving - is the proving of mathematical theorems by a computer program.
  • Mizar - is mathematical library which contains c. 8000 definitions and 50000 theorems.
    Is the biggest library of formal mathematics of all time.

Links

  • Mizar project - Mizar mathematical library
  • KTIML - Department of Theoretical Computer Science and Mathematical Logic
  • TPTP - is a library of test problems for ATP systems

Contact

prof. RNDr. Petr Štěpánek, DrSc.

Department of Theoretical Computer Science and Mathematical Logic
Faculty of Mathematics and Physics, Charles University in Prague
Malostranské nám. 2/25, 118 00 Praha 1
Czech Republic
e-mail: Petr.Stepanek (at) mff.cuni.cz tel: +420221914243 fax: +420221914353