The ρLog calculus

The ρLog calculus performs SLDNF-resolution with leftmost literal selection: every rule $t{\to }_{s}t\text{'}/;con{d}_1\wedge \dots \wedge con{d}_n$ is logically equivalent with the clause

$t{\to }_{s}x/;con{d}_1\wedge \dots \wedge con{d}_n\wedge (t\text{'}\equiv x\_).$

where $x$ is a fresh term variable and we can use resolution with respect to this equivalent clauses. The main difference from resolution in first-order logic is that, instead of using the auxiliary function $mgu(t,t\text{'})$ to compute a most general unifier of two terms, we use the function $mcsm(t,t\text{'})$, which computes the finitely many matchers between a term $t\in T(F,V)$ and a ground term $t\text{'}.$

The calculus has inference rules for the judgment $Q{\rightsquigarrow }_{\sigma }Q\text{'}$ with intended reading "query $Q$ is reducible to $Q\text{'}$ if substitution σ is performed."

We write

$Q_0{\rightsquigarrow }_{\sigma }^{*}{Q}_n$, or just $Q_0{\rightsquigarrow }^{*}{Q}_n$, whenever we succeed to infer a sequence of judgments $Q_0{\rightsquigarrow }_{{\sigma }_1}{Q}_1\dots {\rightsquigarrow }_{{\sigma }_n}{Q}_n$, and $\sigma$ is the restriction of substitution ${\sigma }_1\dots {\sigma }_n$ to $vars\left(Q_0\right)$
• $Q_0{⇸}^{*}{Q}_n$ whenever we finitely fail to infer that $Q_0{\rightsquigarrow }^{*}{Q}_n$ holds.

As usual, the inference rules with respect to a program $P$ have the form $\genfrac{}{}{0.1ex}{}{H_1\dots H_n}{Q{\rightsquigarrow }_{\sigma }Q\text{'}}$ with intended reading "$Q{\rightsquigarrow }_{\sigma }Q\text{'}$ holds iff $H_1$ and ... and $H_{\mathrm{n}}$ hold."
They are:

• $\genfrac{}{}{0.1ex}{}{(t{\text{'}}_1{\to }_{s\text{'}}t{\text{'}}_2/;\underset{i=1}{\overset{n}{\bigwedge }}con{d}_i)\in P\sigma \in mcsm\left(\right(t{\text{'}}_1,s\text{'}),(t_1,s\left)\right)}{\left(t_1{\to }_s{t}_2\right)\wedge Q{\rightsquigarrow }_{\sigma }(\underset{i=1}{\overset{n}{\bigwedge }}con{d}_i\wedge (t{\text{'}}_2\equiv t_2)\wedge Q)}$


• $\genfrac{}{}{0.1ex}{}{\sigma \in mcsm(t\text{'},t)}{(t\equiv t\text{'})\wedge Q{\rightsquigarrow }_{\sigma }\sigma \left(Q\right)}\genfrac{}{}{0.1ex}{}{\sigma \in mcsm(t\text{'},t)}{(t{\to }_{"Id"}t\text{'})\wedge Q{\rightsquigarrow }_{\sigma }\sigma \left(Q\right)}$


• $\genfrac{}{}{0.1ex}{}{(t{\to }_{s}t\text{'}){\nrightarrow }^{*}\top }{(t{\nrightarrow }_{s}t\text{'})\wedge Q{\rightsquigarrow }_{\left\{\right\}}Q}\genfrac{}{}{0.1ex}{}{(t{\to }_{s_1}t\text{'}){\rightsquigarrow }_{\sigma }^{*}\top }{(t{\to }_{Fst[s_1,\dots ]}t\text{'})\wedge Q{\rightsquigarrow }_{\sigma }\sigma \left(Q\right)}\genfrac{}{}{0.1ex}{}{(t{\to }_{s_1}t\text{'}){\nrightarrow }^{*}\top }{(t{\to }_{Fst[s_1,s_2,\dots ,s_n]}t\text{'})\wedge Q{\rightsquigarrow }_{\left\{\right\}}(t{\to }_{Fst[s_2,\dots ,s_n]}t\text{'})\wedge Q}$
   
• $\genfrac{}{}{0.1ex}{}{(t{\to }_s\_){\rightsquigarrow }^{*}\top }{(t{\to }_{NF\left[s\right]}t\text{'})\wedge Q{\rightsquigarrow }_{\left\{\right\}}(t{\to }_{s\circ NF\left[s\right]}t\text{'})\wedge Q}\genfrac{}{}{0.1ex}{}{(t{\to }_s\_){\nrightarrow }^{*}\top \sigma \in mcsm(t\text{'},t)}{(t{\to }_{NF\left[s\right]}t\text{'})\wedge Q{\rightsquigarrow }_{\sigma }\sigma \left(Q\right)}$


• $\genfrac{}{}{0.1ex}{}{cond\text{ is a valid Mathematica formula}}{cond\wedge Q{\rightsquigarrow }_{\left\{\right\}}Q}$

The proper interpretation of the other composite strategies and predefined parametric strategies is guaranteed by assuming that $P$ contains defining rules for them. For example, the rules for the strategy combinators of ρLog are:
$x\_{\to }_{s1\_\circ s2\_}z/;(x{\to }_{s1}y\_)\wedge (y{\to }_{s2}z\_).$
$x\_{\to }_{s1\_\mid s2\_}z/;\left(x{\to }_{s1}z\_\right).$
$x\_{\to }_{s1\_\mid s2\_}z/;\left(x{\to }_{s2}z\_\right).$
$x\_{\to }_{{s\_}^{*}}y/;\left(x{\to }_{"Id"\mid s\circ s^{*}}y\_\right).$

The list of answers computed by ρLog for a query $Q$ is $An{s}_P\left(Q\right):=\{\sigma \mid$ there is an inference derivation $Q{\rightsquigarrow }_{\sigma }^{*}\top \}.$