Vision-language models (VLMs) often fail on abstract visual reasoning benchmarks such as Bongard problems, raising the question of whether the main bottleneck lies in reasoning or representation.We study this on Bongard-LOGO, a synthetic benchmark of abstract concept learning with ground-truth generative programs, by comparing end-to-end VLMs on raw images with large language models (LLMs) given symbolic inputs derived from those images.Using symbolic inputs as a diagnostic probe rather than a practical multimodal architecture, our Componential-Grammatical (C-G) paradigm reformulates Bongard-LOGO as a symbolic reasoning task based on LOGOstyle action programs or structured descriptions.LLMs achieve large and consistent gains, reaching mid-90s accuracy on Free-form problems, while a strong visual baseline remains near chance under matched task definitions.Ablations on input format, explicit concept prompts, and minimal visual grounding show that these factors matter much less than the shift from pixels to symbolic structure.These results identify representation as a key bottleneck in abstract visual reasoning and show how symbolic input can serve as a controlled diagnostic upper bound.

Most high-end automated theorem provers for first order logic (FOL) split available time between short runs of a large portfolio of search strategies. These runs are typically independent and can be parallelized to exploit all the available processor cores. We explore several avenues of re-using clauses generated by earlier runs and present experimental results of their usefulness or lack thereof.

Abstract We describe an experimental implementation of a logic-based end-to-end pipeline of performing inference and giving explained answers to questions posed in natural language. The main components of the pipeline are semantic parsing, integration with large knowledge bases, automated reasoning using extended first order logic, and finally the translation of proofs back to natural language. While able to answer relatively simple questions on its own, the implementation is targeting research into building hybrid neurosymbolic systems for gaining trustworthiness and explainability. The end goal is to combine machine learning and large language models with the components of the implementation and to use the automated reasoner as an interface between natural language and external tools like database systems and scientific calculations.

Abstract Commonsense reasoning has long been considered one of the holy grails of artificial intelligence. Our goal is to develop a logic-based component for hybrid – machine learning plus logic – commonsense question answering systems. A critical feature for the component is estimating the confidence in the statements derived from knowledge bases containing uncertain contrary and supporting evidence obtained from different sources. Instead of computing exact probabilities or designing a new calculus we focus on extending the methods and algorithms used by the existing automated reasoners for full classical first-order logic. The paper presents the CONFER framework and implementation for confidence estimation of derived answers.

Mining crowd-sourced movement trajectories is a useful tool in urban computing. Common mobility patterns of the visitors or residents of a city can be exploited in applications such as disaster management, transportation planning and ad placement. In recommendation systems, individual behaviour is of special interest. To extract the visiting behaviour of individuals, the trajectories need to be semantically annotated. We describe how hierarchical regions of interest (ROIs) can be used for semantic annotation. By combining multiple layers of smaller and larger regions we can flexibly detect both visits to dense hotspots and trajectory segments visiting larger areas, such as an old town, a park or an island. Extending the annotation beyond common hotspots captures more information about the behaviour.

The paper presents sound and complete translations of several fragments of Martin-Löf's monomorphic type theory to first-order predicate calculus. The translations are optimized for the purpose of automated theorem proving in the mentioned fragments. The implementation of the theorem prover Gandalf and several experimental results are described.

We argue that decidable classes of predicate logic combhted with efficient decision methods are a suitable basis for developing powerful knowledge representation languages.The paper presents some methods for developing such languages based on decidable classes.Queries can be answered and databases can be completed by using efficient dectilon refinements of the resolution method.Severaf decidable classes usable as new knowledge representation languages are presented, cent aining some well-known ones, like the base language ALC of KL-ONE type systems, along with the resolution-based inference engines.

We investigate the problem of finding a computable witness for the existential quantifier in a formula of the classical first-order predicate logic. The A-resolution calculus which is essentially the same as the program derivation algorithm A of C.-L. Chang, R.C-T. Lee and R.Waldinger is used for finding a definite substitution t for an existentially bound variable y in some formula F, such that F{t/y} is provable. The term t is built of the function and predicate symbols in F, plus Boolean functions and a case splitting function if, defined in the standard way: if (True, x,y) = x and if(False, x,y) = y. We prove that the A-resolution calculus is complete in the following sense: if such a definite substitution exists, then the A-calculus derives a clause giving such a substitution. The result is strengthened by allowing the usage of liftable criteria R of a certain type, prohibitin the derivation of the substitution terms t for which R(t) fails. The enables us to specify, for example, that the substitution t must be in some special signature or must be type-correct, without losing completeness. We will also consider ordering restrictions for the A-calculus.