ISSUE-579: Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic

declarative-fol-specification

Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic

State:

CLOSED

Product:

Formal Semantics

Raised by:

James Cheney

Opened on:

2012-10-25

Description:

A sub-issue of ISSUE-576.

From Antoine Zimmermann's email:
http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html

The document tries to define a kind of semantics for the PROV-DM, but it's not actually defining a proper semantics at all. And since it does not truly define a formal semantics, it has to redefine the terms that are borrowed from logic, and subtly diverge from the standard notions found in logic. For someone who knows about logic, it makes the document larger, more complicated than it should be, more difficult to read, and more difficult to implement. For someone who does not know about logic, it's not made at all simpler, on the contrary.

...

If a proper semantics was defined, there would be no way the document diverge from legacy logical concepts. There would be less chances for mistakes in the definitions and in the rules laters. There would be more flexibililty in the way implementations support the semantics.

I see two escapes for this:
1) define an ad hoc model theory for PROV-DM, in the line of what's sketched in PROV-SEM;
2) rely on a well known logic (such as FOL), to which all PROV statements are mapped, and add FOL axioms to model the constraints.

1) is ambitious and I understand there is not enough time to investigate it enough. But 2) is really easy. PROV statements already look a lot like FOL predicates, and PROV Constraints already rely heavily on FOL notions and notations.

Related Actions Items:

No related actions

Related emails:

1. Re: PROV-ISSUE-579 (declarative-fol-specification): Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic [prov-dm-constraints] (from jcheney@inf.ed.ac.uk on 2013-04-11)
2. Re: PROV-SEM staged, ready for review (from Khalid.Belhajjame@cs.man.ac.uk on 2013-04-11)
3. Re: PROV-SEM staged, ready for review (from jcheney@inf.ed.ac.uk on 2013-04-11)
4. Re: PROV-SEM staged, ready for review (from jcheney@inf.ed.ac.uk on 2013-04-11)
5. Re: PROV-SEM staged, ready for review (from satya.sahoo@case.edu on 2013-04-10)
6. Re: PROV-SEM staged, ready for review (from tom.denies@ugent.be on 2013-04-10)
7. Re: PROV-SEM staged, ready for review (from Khalid.Belhajjame@cs.man.ac.uk on 2013-04-09)
8. RE: PROV-SEM staged, ready for review (from simon.miles@kcl.ac.uk on 2013-04-09)
9. Re: PROV-SEM staged, ready for review (from l.moreau@ecs.soton.ac.uk on 2013-04-08)
10. PROV-SEM staged, ready for review (from jcheney@inf.ed.ac.uk on 2013-04-05)
11. Re: PROV-ISSUE-579 (declarative-fol-specification): Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic [prov-dm-constraints] (from jcheney@inf.ed.ac.uk on 2013-03-08)
12. Re: PROV-WG response to comments on constraints (from jcheney@inf.ed.ac.uk on 2012-11-06)
13. Re: PROV-WG response to comments on constraints (from jcheney@inf.ed.ac.uk on 2012-11-01)
14. Re: PROV-WG response to comments on constraints (from antoine.zimmermann@emse.fr on 2012-11-01)
15. PROV-WG response to comments on constraints (from jcheney@inf.ed.ac.uk on 2012-11-01)
16. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from l.moreau@ecs.soton.ac.uk on 2012-11-01)
17. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-11-01)
18. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from l.moreau@ecs.soton.ac.uk on 2012-11-01)
19. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-11-01)
20. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from p.t.groth@vu.nl on 2012-11-01)
21. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-10-31)
22. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from l.moreau@ecs.soton.ac.uk on 2012-10-31)
23. Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-10-31)
24. Re: Review of PROV-CONSTRAINTS issues (ISSUE-582, ISSUE-579, ISSUE-585, ISSUE-583) (from Paolo.Missier@ncl.ac.uk on 2012-10-29)
25. Review of PROV-CONSTRAINTS issues (ISSUE-582, ISSUE-579, ISSUE-585, ISSUE-583) (from jcheney@inf.ed.ac.uk on 2012-10-26)
26. PROV-ISSUE-579 (declarative-fol-specification): Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic [prov-dm-constraints] (from sysbot+tracker@w3.org on 2012-10-25)

Related notes:

No additional notes.

Display change log