Fwd: pmlj:hasDischarge example

[Timothy Lebo]

Paulo,

Will you be able to use this example to explain discharge to me during the IW call today?

Thanks,

Tim

Begin forwarded message:

From: c chang <c...@cs.rpi.edu>

Subject: pmlj:hasDischarge example

Date: September 12, 2013 5:35:57 PM EDT

To: Timothy Lebo <le...@rpi.edu>, Jim McCusker <mcc...@rpi.edu>, "Deborah L. McGuinness" <d...@cs.rpi.edu>, Paulo Pinheiro <pp3...@gmail.com>

Example: http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001%2B1%2FEP---1.2%2Fanswer.owl%23answer

Please take a look at nodesets 47 and 48:


You can see the assumption and its negation.

And then take look towards the final conclusion of nodesets 1 and 2:



From nodeset 2 to 1, the refutation rule discharged nodeset 47 to prove nodeset 48.

Also see the summary view (be sure to click the "show" button of the "Justified by") :

http://browser.inference-web.org/iwbrowser/BrowseNodeSet?uri=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001%2B1%2FEP---1.2%2Fanswer.owl%23answer

Thanks,

csc

[Timothy Lebo]

We were able to work through the structure of a Refutation plan to produce a discharge:

http://inference-web.org/wiki/IW_Meeting_2013-10-03#Discussions

We did not work through any of the spreadsheet proposals. I wore Paulo out too much ;-)

We'll pick that up next week. Meanwhile, feel free to look them over so that we're prepared to knock them out quickly:

http://inference-web.org/wiki/IW_Meeting_2013-10-03#ledToAnswer

@Paulo, are you on the inference web list with a personal email address?

Thanks,

Tim

On Oct 3, 2013, at 10:20 AM, Timothy Lebo <le...@rpi.edu> wrote:

Paulo,

Will you be able to use this example to explain discharge to me during the IW call today?

Thanks,

Tim

Begin forwarded message:

From: c chang <c...@cs.rpi.edu>

Subject: pmlj:hasDischarge example

Date: September 12, 2013 5:35:57 PM EDT

To: Timothy Lebo <le...@rpi.edu>, Jim McCusker <mcc...@rpi.edu>, "Deborah L. McGuinness" <d...@cs.rpi.edu>, Paulo Pinheiro <pp3...@gmail.com>

Example: http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001%2B1%2FEP---1.2%2Fanswer.owl%23answer

Please take a look at nodesets 47 and 48:

<Screen shot 2013-09-12 at 2.23.27 PM.png>

You can see the assumption and its negation.

And then take look towards the final conclusion of nodesets 1 and 2:

<Screen shot 2013-09-12 at 2.27.05 PM.png>

From nodeset 2 to 1, the refutation rule discharged nodeset 47 to prove nodeset 48.

Also see the summary view (be sure to click the "show" button of the "Justified by") :

http://browser.inference-web.org/iwbrowser/BrowseNodeSet?uri=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001%2B1%2FEP---1.2%2Fanswer.owl%23answer

Thanks,

csc

--
You received this message because you are subscribed to the Google Groups "inference-web" group.
To unsubscribe from this group and stop receiving emails from it, send an email to inference-we...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.