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 system for automated reasoning over such knowledge bases - MaLARea - has won the Large-Theory (LTB) division of the world automated reasoning championship (CASC-24) in 2013. Our systems MaLARea and SInE have won two categories in the world automated reasoning championship (CASC-J4) 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.

The first prize in CASC-24 LTB DIVISION

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. (†2012)

department: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
research areas: Formal methods, declarative programming, logic
DBLP
Josef Urban

Mgr. Josef Urban, Ph.D.

department: CIIRC, Czech Technical University in Prague
e-mail: Josef.Urban (at) gmail.com
www: http://people.ciirc.cvut.cz/~urbanjo3
research areas: Automated Reasoning, inductive reasoning, formalization and computer-verification of mathematics
DBLP
Jiří Vyskočil

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

department: CIIRC, Czech Technical University in Prague
e-mail: jiri.vyskocil (at) gmail.com
www: http://people.ciirc.cvut.cz/~vyskoji1
research areas: Automated Reasoning
DBLP
Jan Jakubův

Mgr. Jan Jakubův, Ph.D.

department: CIIRC, Czech Technical University in Prague
e-mail: jakubuv (at) gmail.com
www: http://people.ciirc.cvut.cz/~jakubja5
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

Dr. RNDr. Ondřej Kunčar

department: Chair for Logic and Verification, Technische Universität München, Germany
e-mail: kuncar (at) in.tum.de
www: https://www21.in.tum.de/~kuncar/
research areas: Interactive theorem proving, security in-the-large
DBLP
Chad E Brown

Chad E Brown, Ph.D.

department: CIIRC, Czech Technical University in Prague
e-mail: not applicable
www:
research areas: Higher-Order Theorem Proving, Semantics of Higher-Order Logic, Generalizations of Henkin Models, Extensionality Principles, Set Comprehension Principles, Cut-Elimination, Completeness and Independence Results, Automatic and Interactive Theorem Proving, Proof Checking, Proof Representations and Transformations
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

Selected Publications

  • Theorem Proving in Large Formal Mathematics as an Emerging AI Field.
    Josef Urban, Jiří Vyskočil, Essays in Memory of William McCune, LNAI 7788: 240-257 (2013)
  • Automatické uvažování (Automated Reasoning).
    Josef Urban, Jiří Vyskočil, Petr Štěpánek. In Olga Štěpánková et al., editor, Umělá Inteligence 6 (Artificial Intelligence 6), book chapter: 249-278 (2013)
  • Proving Valid Quantified Boolean Formulas in HOL Light.
    Ondřej Kunčar. ITP 2011: 184-199
  • MaLeCoP: Machine Learning Connection Prover.
    Josef Urban, Jiří Vyskočil, Petr Štěpánek. TABLEAUX 2011: 263-277
  • 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

Contact


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

Czech Institute of Informatics, Robotics, and Cybernetics
Czech Technical University in Prague
Zikova 1903/4
166 36 Prague 6
Czech Republic
e-mail: vyskoji1 (at) fel.cvut.cz

Mgr. Josef Urban, Ph.D.

e-mail: Josef.Urban (at) gmail.com
www: http://cs.ru.nl/~urban/