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.
Logic-based computer science is the most exciting field of our times. (Bruno Buchberger)
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
Mgr. Josef Urban, Ph.D.department: CIIRC, Czech Technical University in Prague
e-mail: Josef.Urban (at) gmail.com
research areas: Automated Reasoning, inductive reasoning, formalization and computer-verification of mathematics
RNDr. Jiří Vyskočil, Ph.D.department: CIIRC, Czech Technical University in Prague
e-mail: jiri.vyskocil (at) gmail.com
research areas: Automated Reasoning
Mgr. Jan Jakubův, Ph.D.department: CIIRC, Czech Technical University in Prague
e-mail: jakubuv (at) gmail.com
research areas: Automated Reasoning
RNDr. Petr Pudlák, Ph.D.e-mail: petr (at) pudlak.name
research areas: Automated theorem proving, functional programs, logic systems, Semantic Web
RNDr. David Stanovský, Ph.D.department: Department of Algebra, Charles University in Prague
e-mail: stanovsk (at) karlin.mff.cuni.cz
research areas: General algebra, automated theorem proving
Mgr. Ondřej Kunčardepartment: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
e-mail: ondrej.kuncar (at) mff.cuni.cz
research areas: Computational logic, interactive theorem provers, systems for formal mathematics
Mgr. Vladimír Šišmadepartment: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
e-mail: vsisma (at) sidaaq.cz
research areas: Automated reasoning
RNDr. Martin Sudadepartment: 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
research areas: Automated theorem proving, accessing external functions from prover loop
Bc. Filip Děchtěrenkodepartment: Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague
e-mail: filip.dechterenko (at) gmail.com
research areas: Automated theorem proving
- 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 Quantiﬁed 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)
- 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.