Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

556 users

+1 vote
Let's take [(Fa) SU b] into consideration, seen on slide 70 (printed version).

When calculating SU, we have to replace /var_phi in /phi by q. Later this q is moved to the initial states.

We were wondering how this substitution is done ( we don't know where exactly the 'x' appears and how this results into 'q')
in * TF "Emb. Sys. and Rob." by (490 points)

1 Answer

+3 votes
 
Best answer

I guess that your question refers to the following rules: 

The Φ<α>x means that we consider a formula Φ that may have several occurrences of a subformula α. To denote some of these, we consider a stub/template of Φ where the occurrences of interest are replaced with a new variable x. 

For example, let Φ be the formula (Fa)⋁¬(Fa) that has two occurrences of the subformula Fa. We consider it now as a substitution of variable x in formula x⋁¬x by formula Fa, so Φ=(Fa)⋁¬(Fa), α=Fa. But you may also consider x⋁¬(Fa) and just replace the first occurrence of Fa (for whatever reason).

When we abbreviate one subformula, we can replace this way also other occurrences of the same subformula with the new abbreviation variable, and calling them x, we can control which of them should be abbreviated.

So, you can decide which of the occurrences you want to call x, means you want to replace with the new abbreviation this way. Ideally, all of them, but sometimes you may not want this.

by (170k points)
edited by

Related questions

Imprint | Privacy Policy
...