Adam Trybus

Adam Trybus, Karolina Rożko, Tomasz Skura

We describe a new method of finding interpolants for classical logic using certain refutation system as a starting point. Refutation can be thought of as an alternative approach to the analysis of formal systems: instead of focusing on which formulas provably belong to a given logic, it shows which formulas are to be rejected. Thus, it provides a mirror proof system. As it turns out, the benefits of such an approach go well beyond the area of refutation calculi themselves. We provide one such example in the shape of an interpolant-searching method. To be sure, a number of such methods are already in use. The novelty of our proposal lies in the fact that it can be considered as based on a non-binary version of resolution.

Adam Trybus

We focus on a branch of region-based spatial logics dealing with affine geometry. The research on this topic is scarce: only a handful of papers investigate such systems, mostly in the case of the real plane. Our long-term goal is to analyse certain family of affine logics with inclusion and convexity as primitives interpreted over real spaces of increasing dimensionality. In this article we show that logics of different dimensionalities must have different theories, thus justifying further work on different dimensions. We then focus on the three-dimensional case, exploring the expressiveness of this logic and consequently showing that it is possible to construct formulas describing a three-dimensional coordinate frame. The final result, making use of the high expressive power of this logic, is that every region satisfies an affine complete formula, meaning that all regions satisfying it are affine equivalent.

Adam Trybus, Bartosz Bartnicki, Remigiusz Kinas

This paper presents a research program dedicated to evaluating and advancing the reasoning capabilities of Bielik, a Polish large language model. The study describes a number of stages of work: initial benchmarking and creation of evaluation methodology, analyzing of comparative results with other LLMs and outlining of future prospects that take into account the limitations of the analyses conducted so far and aims to keep Bielik in the race give the ever-changing -- and competitive -- AI landscape.