Skip to content
Snippets Groups Projects
Commit 6780e409 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

tweak

parent cfeffed7
No related branches found
No related tags found
No related merge requests found
No preview for this file type
......@@ -238,7 +238,7 @@ co-occurring subterms.
To see the full power of unification-based querying, consider a student who encounters
$\int_{\mathbb{R}^2} |\sin(t)\cos(t)| dt$ and wishes to know if there are any mathematical
statements (like theorems, identities, inequalities) that can be applied to it. Indeed,
there are many such statements (for example H\"older's inequality) and they can be found
there are many such statements (for example H\"older's inequality) and they can be founda
using \textbf{generalization queries}. The idea behind answering generalization queries is
that the index marks universal\footnote{We consider an identifier as universal if it can
be instantiated without changing the truth value of the containing expression. In formal
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment