Zobrazeno 1 - 10
of 40
pro vyhledávání: '"Janicic, Predrag"'
Publikováno v:
EPTCS 398, 2024, pp. 21-37
Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjectu
Externí odkaz:
http://arxiv.org/abs/2401.11898
Autor:
Janičić, Predrag, Narboux, Julien
Publikováno v:
EPTCS 352, 2021, pp. 91-102
We report on a new, simple, modular, and flexible approach for automated generation of illustrations for (readable) synthetic geometry proofs. The underlying proofs are generated using the Larus automated prover for coherent logic, and corresponding
Externí odkaz:
http://arxiv.org/abs/2201.00540
Autor:
Janičić, Predrag, Kovács, Zoltán
Publikováno v:
EPTCS 352, 2021
Automated Deduction in Geometry (ADG) is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools at the intersection between geometry and automated deduction. Relevant topics include (but are n
Externí odkaz:
http://arxiv.org/abs/2112.14770
Publikováno v:
Logical Methods in Computer Science, Volume 15, Issue 1 (March 29, 2019) lmcs:4233
There are several approaches for using computers in deriving mathematical proofs. For their illustration, we provide an in-depth study of using computer support for proving one complex combinatorial conjecture -- correctness of a strategy for the che
Externí odkaz:
http://arxiv.org/abs/1801.07528
Publikováno v:
In Journal of Symbolic Computation March-April 2020 97:3-15
We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rules and is based on a frag- ment of first-order logic called coherent lo
Externí odkaz:
http://arxiv.org/abs/1405.3391
Autor:
Marinkovic, Vesna, Janicic, Predrag
Straightedge and compass construction problems are one of the oldest and most challenging problems in elementary mathematics. The central challenge, for a human or for a computer program, in solving construction problems is a huge search space. In th
Externí odkaz:
http://arxiv.org/abs/1207.4432
Publikováno v:
EPTCS 79, 2012, pp. 63-81
We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal verification of the
Externí odkaz:
http://arxiv.org/abs/1202.4831
Autor:
Maric, Filip, Janicic, Predrag
Publikováno v:
Logical Methods in Computer Science, Volume 7, Issue 3 (September 28, 2011) lmcs:843
We present a formalization of modern SAT solvers and their properties in a form of abstract state transition systems. SAT solving procedures are described as transition relations over states that represent the values of the solver's global variables.
Externí odkaz:
http://arxiv.org/abs/1108.4368
The importance of algorithm portfolio techniques for SAT has long been noted, and a number of very successful systems have been devised, including the most successful one --- SATzilla. However, all these systems are quite complex (to understand, reim
Externí odkaz:
http://arxiv.org/abs/1107.0268