reference on relating Post systems to string rewriting systems and formal grammars?

wikipedia states:

Every Post canonical system can be reduced to a string rewriting system (semi-Thue system) […] It has been proved that any Post canonical system is reducible to such a substitution system, which, as a formal grammar, is also called a phrase-structure grammar, or a type-0 grammar in the Chomsky hierarchy

and on a different page:

A semi-Thue system is also a special type of Post canonical system, but every Post canonical system can also be reduced to an SRS.

I have not been able to find much explanation of these statements.

Is there a good reference that shows how to do conversions between these notions?

Proving a first order logic theorem with equational logic with a term rewriting system

I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean Algebra). The target language also permits Skolemization (Sk). So the translation task is from FOL to EL+BL+Sk. My motivation is that if my translation and subsequent proof in EL+BL+Sk are correct, then I should be able to perform such proofs using a Term Rewriting System (TRS). TRS can be used to prove equational theories. Because EL+BL is a sub-logic of FOL and Skolemization results in an equisatisfiable system, it is hoped that a valid proof in EL+BL+Sk is a valid proof of the original FOL theorem. Below is a FOL example and my attempt at a proof using natural deduction. This is followed by my attempt at translation and proof in EL+BL+Sk. See notes on translation/proof below.

My questions are:

Is the tentative translation from FOL to EL+BL+Sk correct?

Is the tentative proof in EL+BL+Sk correct?

Does the proof in EL+BL+Sk count as a proof of the original FOL theorem? I am not sure how proof theoretic entailment ($$\vdash$$) in FOL relates to semantic entailment ($$\models$$) in EL+BL+Sk. Does ($$\Gamma \models_{EL+BL+Sk} \varphi \iff \Gamma \vdash_{FOL} \varphi$$) hold?

Example FOL formulae

At least one person is liked by every person: $$\exists y \forall x :Likes(x,y)$$

Every persons likes at least one person: $$(\forall x \exists y: Likes(x,y))$$

I want to prove: $$(\exists y \forall x: Likes(x,y)) \vdash (\forall x \exists y : Likes(x,y))$$

Natural Deduction (ND) proof

The ND proof uses syntactic consequence where $$\Gamma \vdash \varphi$$ means that the sentence $$\varphi$$ is provable from the set of assumptions $$\Gamma$$. \begin{align*} &\textbf{FOL Theorem}~~(\exists y \forall x :Likes(x,y)) \vdash (\forall x \exists y :Likes(x,y)) \ &\ &\textbf{Notation for EL+BL+Sk}\ &x~~~~~~~~~~~~~~~~~~~~~~~~~\forall x~~\text{Universally Quantified variable}\ &c~~~~~~~~~~~~~~~~~~~~~~~~~~\text{Skolem Constant}\ &d~~~~~~~~~~~~~~~~~~~~~~~~\text{Arbitrary Person , for universal elimination}\ &\mathtt{skFun}~~~~~~~~~~~~~~~~\text{Skolem Function}\ &\mathtt{Likes}~~~~~~~~~~~~~~~~\text{Boolean valued function}\ &\mathtt{true}~~~~~~~~~~~~~~~~~~\text{Boolean constant}\ &\ &\textbf{Translation of Theorem to EL+BL+Sk:}\ &(\forall x :(\mathtt{skFun}(x)=c ,\mathtt{Likes}(x,c)))\models(\forall x:\mathtt{Likes}(x,\mathtt{skFun}(x))) \ &\ &\textbf{Proof in EL+BL+Sk}\ &\textbf{1}~~\forall x:\mathtt{Likes}(x,c) = true~~~~~~\text{Assumption, with Skolem constant c }\ &\textbf{2}~~\forall x:\mathtt{skFun}(x) = c~~~~~~~~~~~~~~~\text{Interpretation of Sk. function with Sk. constant c }\ &\textbf{3}~~\mathtt{Likes}(d,\mathtt{skFun}(d))~~~~~~~~~~~~\text{Universal elim & Skolemization of term to be proved}\ &\textbf{4}=~~~~~\mathtt{Likes(d,c)}~~~~~~~~~~~~~~~~\text{Apply 2 to second argument of 3}\ &\textbf{5}=~~~~~~true~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\text{Apply 1 at 4}\ \end{align*} Notes on translation/proof.

• The EL+BL+Sk proof relies on an interpretation, so the translation needs semantic entailment $$\models$$. In general, this can be written as $$\Gamma \models_{EL+BL+Sk} \varphi$$, which means that under $$EL+BL+Sk$$ logic the sentence $$\varphi$$ is true in all models of $$\Gamma$$.

• In EL all variables are considered to be universally quantified.

• Existential variables in FOL that are not in the scope of universals are translated to Skolem constants.

• Existential variables in FOL that are in the scope of universals are translated to Skolem functions e.g. $$\mathtt{skFun}(x)$$ with single universal argument of $$x$$. The original existential was in the scope $$x$$.

• Each predicate in FOL is translated to a Boolean valued operation in EL+BL+Sk, e.g. predicate $$Likes$$ becomes Boolean operation $$\mathtt{Likes}$$.

• In EL terms are distinct, unless they are made identical or equal by equations.

Here is the listing in CafeOBJ using TRS.

mod LIKES {   [Person]   pred Likes : Person Person         }  op c : -> Person . ops d : -> Person . op skFun : Person -> Person . -- Hypothesis  eq [assumption] : Likes(x:Person,c) = true . eq [skolem] :  skFun(x:Person) =  c . reduce Likes(d,skFun(d)) . --> Gives true 

Right filter for rewriting page statuscode

I am new to developing wordpress plugins. But I am looking to write a fairly simple plugin.

I want to write a plugin that rewrites the returned status code based on some logic that consults a database. It can essentially be boiled down to an access plugin based on custom logic. When authorization fails I want to either return statuscode 403 or redirect to a login page.

But I am struggling to find the right place to hook in. And also the “correct” way of doing it.

The logic is based on a combination of the Page requested, the logged in user and that users role. Using these values I look up information in a database and either render some custom data or want to turn the user away. If the user is logged in I want to return a 403 but if the user is not logged in I want to return a 401. But is that even the right way of doing it in WordPress? I am used to writing APIs and have never written a WordPress plugin.

Should I render a text that says Content not available! instead of a 403 and redirect the user to the login page instead of a 401?

Ideally I would like to separate the logic that renders the data and the logic that authorizes. I would like that to be two different hooks or filters.

I have tried to add a filter on http_response but I can’t get it to do anything. I am in doubt if I should call apply_filter myself or if WordPress does that.

All help is appreciated.

Data Entry or Rewriting From any Image/Scanned Pages to MS Word for \$2

I’m an expert any kind of data entry job. My Services List: * Data Entry * Manual Typing * Retype Scanned Files * Copy and Paste * Copy paste the data from one site to other * PDF to Excel * Word to Excel * PDF to Word Order me me now!

by: jabbarali05
Created: —
Category: Data Entry
Viewed: 227

Need Article Re-Writing Service

Hi, I am looking to rewrite some content which comes default with the page. niche is SEO and has 4000 words in 20x articles. each 200 words.
content are pretty generic SEO topics.

please PM me with the title "Article Rewriting SEO" and include a quote. need both price and turnaround.

Thanks!

Rewriting URL path in nginx without redirecting

For legacy reasons, I have URLs like https://host.example.com/foo.cgi?id=nnn. I want /foo.cgi?id=nnn.html to respond with the contents of a file nnn.html, where nnn is a number that varies.

In nginx, how do I define a custom mapping from URL paths to different file paths without generating redirects? (That is, while I want the contents of nnn.html to be served, I want the browser-visible URL to continue to be foo.cgi?id=nnn.)

Dovecot Configuration: rewriting / key→value lookup for variables; aliasing the domain

I’d like to configure Dovecot in a way so that it dispatches userdb/passwd lookups into domain specific locations, where the domain itself may have several aliases, but all of them direct to the same location.

The Dovecot wiki gives a simple, trivial example

Multiple passwd files

You can use all the variables in the passwd-file filenames, for example:

passdb {   driver = passwd-file   # Each domain has a separate passwd-file:   args = /etc/auth/%d/passwd } 

However this does not take care of the domain aliasing that may take place. For example a company might have the domains example.com and example.org, and would like to alias them to all work with the same file /site/example/mail/passwd.

Assuming the above example, it would require to rewrite the %d variable through some alias lookup or to first alias the domain, before moving on to look up the user and authenticating.

Now I do understand that Dovecot doesn’t treat the domain part in any special way, so I could users just have configure their MUAs using the joint domain alias. However this doesn’t deal with domain aliasing on delivery.

Ideally I could insert some lookup to rewrite the domain part early on, to be used for delivery and authentication. However I don’t see how to do that without crude hacks.

Disable SQL Rewriting doesn’t work for paragraph type

I set view which display some part of node which is restricted for anonymous user. I disabled SQL Rewriting in this case in other to show not logged user content but only text-field works, not paragraphs. Do you have any solution for that? Do you know about that behaviour of paragraph type?

Rewriting ‘From:’ in ssmtp/mail no longer works in Ubuntu 18.04

In Ubuntu 14.04 I had the following system running which is basically described here and also here. One element of this is that the ‘From:’ address is taken from /etc/ssmtp/revaliases:

mainuser:username@gmail.com:smtp.gmail.com:587 

and the ‘username@gmail.com’ was used as ‘From:’ when I issued a mail like echo -e “Hi there” | mail -s Test user@example.com

In a new installation of Ubuntu 18.04, the ‘From:’ is now

 Clearname <username@hostname> 

where clearname is the name string in /etc/passwd, username is the linux username, and hostname is the linux host name (although changing it with ‘hostname’ does not alter the result).

Of course, this e-mail address is not going to work, I would like to supply my real address. It seems like new versions of GMail or SSMTP have broken this useful and essential feature.

I would be grateful for help!

Rewriting complex formal derivatives

Formal derivatives are given by the following formulas

\begin{align} \frac{\partial f}{\partial z} = \frac{1}{2} \bigg( \frac{\partial f}{\partial x} – i\frac{\partial f}{\partial y} \bigg) \ \frac{\partial f}{\partial \overline{z}} = \frac{1}{2} \bigg( \frac{\partial f}{\partial x} + i\frac{\partial f}{\partial y} \bigg) \end{align} I am to rewrite $$\frac{\partial \overline{f}}{\partial z}$$ and $$\frac{\partial \overline{f}}{\partial \overline{z}}$$

How can it be done? Am I to use Riemann — Cauchy equations? If yes how?