automatic connection finding between two expressions

[researcherben]

Given two expressions, e.g., T = 1/f and f = 1/T, and given a set of inference rules, is it feasible to identify the connectivity?

The first search is "is there an inference rule that directly connects these two expressions?" If there isn't, the second search is "are there two steps that relate the two expressions?" Increase the number of searches until you run out of computational capacity.

Within each search, are there heuristics that can bound the number of inference rules? For example in the case above, eliminate all inference rules that

• reference Dirac notation (since these variables do not involve braket or quantum operators) and
• refer to linear algebra (since these are scalars)

Can the dimensionality of the respective expressions be leveraged to narrow which inference rules are tried? In the case above, the dimensions of the variables are time and time^-1. Which inference rules maintain dimension and involve inversion?

[bhpayne]

From https://derivationmap.net/review_derivation/000008/

Example of how to get from T = 1/f to f = 1/T: raise both sides to the -1 power, then swap left and right sides.

Example of how to get from T = 1/f to f = 1/T: multiply both sides by f, then divide both sides by T, then swap left and right sides.

Example of how to get from f = 1/T and \omega = 2 \pi f to \omega = (2 \pi)/T: substitute expr1 into expr2

Example of how to get from T = 1/f and \omega = 2 \pi f to \omega = (2 \pi)/T: raise both sides of expr1 to the -1 power, substitute expr1 into expr2

[bhpayne]

Potential conference where this could be presented: 8th Workshop on Practical Aspects of Automated Reasoning; https://paar2022.github.io/. August 11-12, 2022. PAAR 2022 is associated with the 11th International Joint Conference on Automated Reasoning (IJCAR-2022).

From the announcement:

Topics include but are not limited to:

• automated reasoning in propositional, first-order, higher-order and non-classical logics;
• implementation of provers (SAT, SMT, resolution, tableau, instantiation-based, rewriting, logical frameworks, etc);
• automated reasoning tools for all kinds of practical problems and applications;
• pragmatics of automated reasoning within proof assistants;
• practical experiences, usability aspects, feasibility studies;
• evaluation of implementation techniques and automated reasoning tools;
• performance aspects, benchmarking approaches;
• non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications;
• implementation techniques, optimisation techniques, machine learning, strategies and heuristics, fairness;
• support tools for prover development;
• system descriptions and demos. We are particularly interested in contributions that help the community to understand how to build useful reasoning systems in practice, and how to apply existing systems to real problems.