ISSUE-72: Should Core support some approximation to skolem functions?

Skolem functions in Core

Should Core support some approximation to skolem functions?

State:

CLOSED

Product:

Core

Raised by:

Dave Reynolds

Opened on:

2008-08-21

Description:

It is common in PR systems to create new objects as a result of rules. One current proposal for PRD is that it should support this via a specific syntax:
http://lists.w3.org/Archives/Public/public-rif-wg/2008Aug/0069.html

In LP systems skolem functions are used for a similar end, to remove an existential quantification. Whilst BLD has no special support for skolem functions a plain function symbol can be used.

Given that conceptually there is a shared need here, relevant to many applications, is it possible for Core to support a common mechanism for object introduction?

Possible options here include:

(a) Allow restricted use of function symbols in Core purely for this purpose, constrained so that a PRD system can implement it via object construction.

(b) Define a deterministic gensym builtin.
http://lists.w3.org/Archives/Public/public-rif-wg/2008Aug/0071.html

(c) Define a special syntax (not possible unless we are able to modify BLD or require a translation step to translate Core rules to BLD rules).
http://lists.w3.org/Archives/Public/public-rif-wg/2008Aug/0076.html

(d) No support.

This interacts with issue-70 in that such functions introduce possible non-terminations.

Related Actions Items:

No related actions

Related emails:

1. RE: [Core] PROPOSED Core resolutions from telecon Monday, September 22 (from palbert@ilog.fr on 2008-09-24)
2. RE: [Core] PROPOSED Core resolutions from telecon Monday, September 22 (from pvincent@tibco.com on 2008-09-23)
3. [Core] PROPOSED Core resolutions from telecon Monday, September 22 (from Harold.Boley@nrc-cnrc.gc.ca on 2008-09-23)
4. ISSUE-72 (Skolem functions in Core): Should Core support some approximation to skolem functions? [Core] (from sysbot+tracker@w3.org on 2008-08-21)

Related notes:

Display change log