Content deleted Content added
No edit summary |
m Maintain {{WPBS}} and vital articles: 2 WikiProject templates. Create {{WPBS}}. Keep majority rating "Stub" in {{WPBS}}. Remove 2 same ratings as {{WPBS}} in {{WikiProject Computing}}, {{Maths rating}}. Remove 2 deprecated parameters: field, historical. Tag: |
||
| (5 intermediate revisions by 2 users not shown) | |||
Line 1:
{{WikiProject banner shell|class=Stub|
{{WikiProject Computing|
{{WikiProject Mathematics| importance = low}}
}}
Line 20 ⟶ 15:
:the problem is not being too technical. It's about missing the definition of "ground instance". The article is written accessibly enough that I get the feeling if it were defined, things would be a lot clearer. I'll add the appropriate tag and remove the inappropriate technical tag. --[[User:C S|C S]] ([[User talk:C S|talk]]) 12:12, 25 October 2008 (UTC)
==Sloppy algorithm description==
Meanwhile, [[ground instance]] has a redirect link. However, ground instance don't have any variables, so the "last part" doesn't make sense in the current form. I don't have access to the original article, but I guess ''"generate all propositional ground instances"'' is a sloppy phrase for ''"generate all ground instances; for each of them, replace each ground atom by a unique propositional variable"''.
As an example, starting from
:∀''x''. ∃''y''. ''y''>''x'' ∧ ''p''(''y''),
we get after quantifier elimination (i.e. [[Skolemization]], with ''f'' being a Skolem function for ''y''):
:''f''(''x'')>''x'' ∧ ''p''(''f''(''x'')),
which has the ground instances (assuming, e.g., natural numbers' constructors - I'm not sure about this point):
:''f''(0)>0 ∧ ''p''(''f''(0)),
:''f''(''s''(0))>''s''(0) ∧ ''p''(''f''(''s''(0))),
:''f''(''s''(''s''(0)))>''s''(''s''(0)) ∧ ''p''(''f''(''s''(''s''(0)))),
:''f''(''s''(''s''(''s''(0))))>''s''(''s''(''s''(0))) ∧ ''p''(''f''(''s''(''s''(''s''(0))))),
:...
(that is the meaning of "one by one": there may be infinitely many ground instances, all of which have to be checked in succession until an unsatisfiable one is found).
To check e.g. the first one, convert it into a propositional formula by introducing ''A'' for ''f''(0)>0, and ''B'' for ''p''(''f''(0)), leading to
:''A'' ∧ ''B''
which is then shown to be satisfiable by the "last part" (there is nothing to resolve here; however [[:de:Davis-Putnam-Verfahren#Regeln]] lists several other rules, the One-Literal rule would be applicable). In this, admittedly poor, example, all ground instances lead to the propositional formula ''A''∧''B''. - [[User:Jochen Burghardt|Jochen Burghardt]] ([[User talk:Jochen Burghardt|talk]]) 21:28, 21 May 2015 (UTC)
| |||