Artificial intelligence (AI) and large language models (LLM) are reshaping science, with most recent advances culminating in fully-automated scientific discovery pipelines. But qualitative research has been left behind. Researchers in qualitative methods are hesitant about AI adoption. Yet when they are willing to use AI at all, they have little choice but to rely on general-purpose tools like ChatGPT to assist with interview interpretation, data annotation, and topic modeling - while simultaneously acknowledging these system's well-known limitations of being biased, opaque, irreproducible, and privacy-compromising. This creates a critical gap: while AI has substantially advanced quantitative methods, the qualitative dimensions essential for meaning-making and comprehensive scientific understanding remain poorly integrated. We argue for developing dedicated qualitative AI systems built from the ground up for interpretive research. Such systems must be transparent, reproducible, and privacy-friendly. We review recent literature to show how existing automated discovery pipelines could be enhanced by robust qualitative capabilities, and identify key opportunities where safe qualitative AI could advance multidisciplinary and mixed-methods research.

Simulations offer a valuable tool for exploring stimulus equivalence (SE), yet the potential of reject relations to disrupt the assessment of equivalence class formation is contentious. This study investigates the role of reject relations in the acquisition of stimulus equivalence using computational models. We examined feedforward neural networks (FFNs), bidirectional encoder representations from transformers (BERT), and generative pre-trained transformers (GPT) across 18 conditions in matching-to-sample (MTS) simulations. Conditions varied in training structure (linear series, one-to-many, and many-to-one), relation type (select-only, reject-only, and select-reject), and negative comparison selection (standard and biased). A probabilistic agent served as a benchmark, embodying purely associative learning. The primary goal was to determine whether artificial neural networks could demonstrate equivalence class formation or whether their performance reflected associative learning. Results showed that reject relations influenced agent performance. While some agents achieved high accuracy on equivalence tests, particularly with reject relations and biased negative comparisons, this performance was comparable to the probabilistic agent. These findings suggest that artificial neural networks, including transformer models, may rely on associative strategies rather than SE. This underscores the need for careful consideration of reject relations and more stringent criteria in computational models of equivalence.

Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) We use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.

In the realm of formal theorem proving, the Coq proof assistant stands out for its rigorous approach to verifying mathematical assertions and software correctness. Despite the advances in artificial intelligence and machine learning, the specialized nature of Coq syntax and semantics poses unique challenges for Large Language Models (LLMs). Addressing this gap, we present a comprehensive dataset specifically designed to enhance LLMs' proficiency in interpreting and generating Coq code. This dataset, derived from a collection of over 10,000 Coq source files, encompasses a wide array of propositions, proofs, and definitions, enriched with metadata including source references and licensing information. Our primary aim is to facilitate the development of LLMs capable of generating syntactically correct and semantically meaningful Coq constructs, thereby advancing the frontier of automated theorem proving. Initial experiments with this dataset have showcased its significant potential; models trained on this data exhibited enhanced accuracy in Coq code generation. Notably, a particular experiment revealed that a fine-tuned LLM was capable of generating 141 valid proofs for a basic lemma, highlighting the dataset's utility in facilitating the discovery of diverse and valid proof strategies. This paper discusses the dataset's composition, the methodology behind its creation, and the implications of our findings for the future of machine learning in formal verification. The dataset is accessible for further research and exploration: https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1

Analogical proportions are expressions of the form ``$a$ is to $b$ what $c$ is to $d$'' at the core of analogical reasoning. This paper contributes to the mathematical foundations of analogical proportions in the axiomatic tradition as initiated by Yves Lepage two decades ago. For this we introduce proportoids as sets endowed with a 4-ary analogical proportion relation $a:b::c:d$ satisfying a suitable set of axioms and study different kinds of proportion-preserving mappings and relations and their properties.

Analogy-making is at the core of human intelligence and creativity with applications to such diverse tasks as commonsense reasoning, learning, language acquisition, and story telling. This paper studies analogical proportions between booleans of the form `$a$ is to $b$ what $c$ is to $d$' called boolean proportions. Technically, we instantiate an abstract algebraic framework of analogical proportions -- recently introduced by the author -- in the boolean domain consisting of the truth values true and false together with boolean functions. It turns out that our notion of boolean proportions has appealing mathematical properties and that it coincides with a prominent model of boolean proportions in the general case. In a broader sense, this paper is a further step towards a theory of analogical reasoning and learning systems with potential applications to fundamental AI-problems like commonsense reasoning and computational learning and creativity.

Recent success of Bayesian methods in neuroscience and artificial intelligence gives rise to the hypothesis that the brain is a Bayesian machine. Since logic, as the laws of thought, is a product and practice of the human brain, it leads to another hypothesis that there is a Bayesian algorithm and data-structure for logical reasoning. In this paper, we give a Bayesian account of entailment and characterize its abstract inferential properties. The Bayesian entailment is shown to be a monotonic consequence relation in an extreme case. In general, it is a sort of non-monotonic consequence relation without Cautious monotony or Cut. The preferential entailment, which is a representative non-monotonic consequence relation, is shown to be maximum a posteriori entailment, which is an approximation of the Bayesian entailment. We finally discuss merits of our proposals in terms of encoding preferences on defaults, handling change and contradiction, and modeling human entailment.

Recently, I've been spending a lot of time thinking about AI. It's understandable because the technology is quickly seeping into every corner of modern life, present in everything from Autonomous Vehicles to I-phone's Siri. As AI automates repetitive tasks, adds intelligence to existing products, achieves impossible accuracy, and adapts through progressive learning it will become the most important technological phenomena of the 22nd century -- second, perhaps, only to the Blockchain. The exact definition of AI is hotly debated and there are already many fantastic explanations of AI on the internet, so I won't dive in too deeply. But broadly speaking, AI is advanced statistics and applied mathematics which harnesses new advances in computing power and the explosion of available data to give computers new powers of inference, recognition, and choice. Machine learning (ML), the most promising subset of AI, is a field that aims to teach computers to learn from examples (or "Data") and perform a task without being explicitly programmed to do so.

Robinson, J.A. (1965) A machine-oriented logic based on the resolution principle.

Knowing whether a proposition is true means knowing that it is true or knowing that it is false. In this paper, we study logics with a modal operator Kw for knowing whether but without a modal operator K for knowing that. This logic is not a normal modal logic, because we do not have Kw (phi -> psi) -> (Kw phi -> Kw psi). Knowing whether logic cannot define many common frame properties, and its expressive power less than that of basic modal logic over classes of models without reflexivity. These features make axiomatizing knowing whether logics non-trivial. We axiomatize knowing whether logic over various frame classes. We also present an extension of knowing whether logic with public announcement operators and we give corresponding reduction axioms for that. We compare our work in detail to two recent similar proposals.