Workshop taking place 5-7th December, University of Oxford Automated Reasoning in the Age of the Internet The internet hosts a vast store of information that we cannot and should not ignore. It’s not enough just to retrieve facts, to make full use of the internet we must also infer new information from old. This is an exciting new opportunity for automated reasoning, but it also presents new kinds of research challenge. There are a huge number of potential axioms from which to infer new theorems. Methods of choosing appropriate axioms are needed. Information is stored on the internet in diverse forms, and must be curated into a common format before we can apply inference to it. Some of the information is in a depleted state, e.g., RDF triples, and needs to be augmented with additional information, such as time, units, etc. We can employ forms of inference that are novel in automated reasoning, such as using regression to form new functions from sets of number pairs, and then extrapolation to predict new pairs. Information is of mixed quality and accuracy, so introduces uncertainty into the theorems inferred. Some inference methods, such as regression, also introduce uncertainty. Uncertainty estimates need to be inherited during inference and reported to users in an intelligible form. We will report on Kobby Nuamah’s RIF system that explores this new research direction. This article was published on 2024-11-22
