Sören Möller
Theoretical Computer Science / Formal Methods, University of Kassel, Germany
Motivation. Formal verification, the use of mathematical logic and automated reasoning to establish system properties with mathematical rigour, spans techniques from timed model checking and SMT-based reasoning to probabilistic and reactive systems. This work contributes a new domain: the automated verification of hypotheses about natural science experiments in secondary education. Such an experiment can be understood as a network of pairwise dependencies between continuously changing quantities; reasoning compositionally, verifying pairs independently and combining results to handle transitive and indirect interactions, connects this setting naturally to techniques from concurrency and reactive systems. When students conduct a physics or chemistry experiment, they form conjectures, for example that pressure decreases monotonically with altitude, or that oxygen saturation increases with air pressure, and a verification tool should decide whether such a conjecture is a logical consequence of the observed data, producing a counterexample when it is not. A key challenge is that real-world measurements are inherently imprecise: instrument tolerances and environmental noise mean the system under analysis is not a single function but a class of functions consistent with observed bounds. The educational context imposes further requirements: it is not enough to produce a counterexample, as explanations of why a hypothesis fails must be pedagogically meaningful, and responses must appear within seconds for classroom use.
Approach. We model an experiment as a set of real-valued functions over a fixed variable set, where each F(a,b) describes the influence of variable a on b. A scheme is a finite collection of statements constraining a function’s values over an interval while prescribing qualitative behaviour (monotonically increasing, decreasing, or constant), and thus describes the class of experiments consistent with observed data up to measurement tolerances. A hypothesis is itself a single statement; the central problem asks whether it holds for all experiments described by the scheme, a notion we call formal consequence [1]. The first decision procedure [1] introduced a proof calculus operating directly on schemes, but turned out to be incomplete; the second [2] established decidability via a finite abstraction of the uncountable function space, but is far from practical. The present work revisits the proof-calculus approach, extending the calculus of [1] with new inference rules to close the completeness gap, and optimising proof search to run in polynomial time.
Results and open work. We present the extended calculus together with soundness and partial completeness results, and discuss proof search complexity and directions for counterexample extraction. As a complexity-theoretic boundary, the consequence problem is coNP-complete when the variable set is treated as a parameter. Soundness follows directly, as each inference rule is verified individually. Completeness requires the construction of witness functions that satisfy a scheme but falsify a given hypothesis, and remains ongoing work. Finally, an integration with SMT solvers is of interest: beyond aiding completeness arguments, it would allow the consequence problem to be decided over different background theories, and enable counterexample witnesses to be presented to students as pedagogical feedback.
-
Florian Bruse, Martin Lange, and Sören Möller. In: Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings. Lecture Notes in Computer Science. Springer, 2023, pp. 153–169.
-
Sören Möller, Florian Bruse, and Martin Lange. In: Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings. Lecture Notes in Computer Science. Springer, 2025, pp. 346–363.