Notes taken from ‘A Generative Inquiry Dialogue System’ (2007), by Elizabeth Black and Anthony Hunter
5, Soundness and Completeness
5.1, The argument inquiry outcome of a dialogue is a function… if D is a well-formed argument inquiry dialogue with participants x1 and x2, then… (given D the outcome is the set of all arguments that can be constructed from the union of the commitment stores and whose claims are in the question store).
… The benchmark that we compare the outcome of the dialogue with is the set of arguments that can be constructed from the union of the two agents’ beliefs. So this benchmark is, in a sense, the ‘ideal situation’ where there are clearly no constraints on the sharing of beliefs.
5.2, Let D be a well-formed argument inquiry dialogue with participants x1 and x2. We say that D is sound if and only if… (when the outcome of the dialogue includes an argument, then that same argument can be constructed from the union of the two participating agents’ beliefs).
(Theorem 5.1) If D is a well-formed argument inquiry dialogue with participants x1 and x2, then D is sound. Proof: …
5.3, Let D be a well-formed argument inquiry dialogue with participants x1 and x2. We say that D is complete iff… (if the dialogue terminates at t and it is possible to construct an argument for a literal in the question store from the union of the two participating agents’ beliefs, then that argument will be in the outcome of the dialogue at t.)
(Theorem 5.2) If D is a well-formed argument inquiry dialogue with participants x1 and x2, then D is complete. Proof: …
6, Future work…
… We would like to allow more than two agents to take part in an argument inquiry dialogue…
We currently assume that an agent’s belief base does not change during a dialogue, and would like to consider the implication of dropping this assumption…
We would also like to further explore the benchmark which we compare our dialogue outcomes to…
… We would like to further investigate the utility of argument inquiry dialogues when embedded in dialogues of different types.
7, Conclusions…
Saturday, 31 March 2007
15.4, A Generative Inquiry Dialogue System
Notes taken from ‘A Generative Inquiry Dialogue System’ (2007), by Elizabeth Black and Anthony Hunter
4, Dialogue System
The communicative acts in a dialogue are called moves. We assume that there are always exactly two agents (participants) taking part in a dialogue… Each participant takes its turn to make a move to the other participant…
A move in our system is of the form (Agent, Act, Content)… e.g. (x, ‘open’, belief), (x, ‘assert’, (support, conclusion)), (x, ‘close’, belief)…
4.1, A dialogue… is a sequence of moves of the form… (The first move of a dialogue… must always be an open move…, every move of the dialogue must be made to a participant of the dialogue…, and the agents take it in turns to receive moves…)
4.2, (Terminology that allows us to talk about the relationship between two dialogues: ‘Sub-dialogue of’…, ‘top-level dialogue’…, ‘top-dialogue of’…, and ‘extends’…)
4.3, Let D be a dialogue with participants x1 and x2 such that topic(D) = gamma. We say that m(s)… is a matched-closed for D iff m(s-1) = (P, close, gamma) and m(s) = (~P, close, gamma).
So a matched-close will terminate a dialogue D but only if D has not already terminated and any sub-dialogues that are embedded within D have already terminated.
4.4, Let D be a dialogue. D terminates at t iff the following conditions hold…
4.5, The current dialogue is… (the innermost dialogue that has not yet terminated).
We adopt the standard approach of associating a commitment store with each agent participating in a dialogue. A commitment store is a set of beliefs that the agent has asserted so far in the course of the dialogue. As commitment stores consist of things that the agent has already publicly declared, its contents are visible to the other agent participating in the dialogue. For this reason, when constructing an argument, an agent may make use of not only its own beliefs but also those from the other agent’s commitment store.
4.6, A commitment store associated with an agent… is a set of beliefs.
An agent’s commitment store grows monotonically over time. If an agent makes a move asserting an argument, every element of the support is added to the agent’s commitment store. This is the only time the commitment store is updated.
4.7, Commitment store update…
… when an argument inquiry dialogue with topic ‘alpha1 ^ … ^ alphaN -> phi’ is opened, a question store associated with that dialogue is created whose contents are {alpha1, …, alphaN}. Throughout the dialogue the participant agents will both try to provide arguments for the literals in the question store. This may lead them to open further nested argument inquiry dialogues that have a topic a rule consequent is a literal in the question store.
4.8… a question store… is a finite set of literals such that…
A protocol is a function that returns the set of moves that are legal for an agent to make at a particular point in a particular type of dialogue…
4.9, The argument inquiry protocol is a function (that takes the top-level dialogue that the agents are participating in and the identifier of the agent whose turn it is to move, and returns the set of legal moves that the agent can make)…
(An agent can only assert an argument or open a rule for a conclusion that is in the current Question Store, and such that the move has not been made by either agent at an earlier timepoint in the dialogue.)
Note that it is straightforward to check conformance with the protocol as the protocol only refers to public elements of the dialogue.
… a specific strategy function… allows an agent to select exactly one legal move to make at each timepoint in an argument inquiry dialogue. A strategy is personal to an agent and the move that it returns depends on the agent’s private beliefs. The argument inquiry strategy states that if there are any legal moves that assert an argument that can be constructed by the agent (by means of its belief base and the other agent’s commitment store) then a single one of those moves is selected…, else if there are any legal open moves with a defeasible rule as their content that is in the agent’s beliefs then a single one of these moves is selected… If there are no such moves then a close move is made.
4.10… The function pickO returns the chosen open move…
4.11… The function pickA returns the chosen assert move…
4.12, The argument inquiry strategy is a function (that takes the top-level dialogue that the agents are participating in and the identifier of the agent whose turn it is to move, and returns exactly one of the legal moves)…
Note that a top-level argument inquiry dialogue will always have a defeasible fact as its topic, but each of its sub-dialogues will always have a defeasible rule as its topic.
4.13, D is a well-formed argument inquiry dialogue iff… (D does not continue after it has terminated and is generated by the argument inquiry strategy).
… Note that we assume some higher-level planning component that guides the agent when deciding whether to enter into a dialogue, who this dialogue should be with and on what topic, i.e. that makes the decision to make the move m1.
4, Dialogue System
The communicative acts in a dialogue are called moves. We assume that there are always exactly two agents (participants) taking part in a dialogue… Each participant takes its turn to make a move to the other participant…
A move in our system is of the form (Agent, Act, Content)… e.g. (x, ‘open’, belief), (x, ‘assert’, (support, conclusion)), (x, ‘close’, belief)…
4.1, A dialogue… is a sequence of moves of the form… (The first move of a dialogue… must always be an open move…, every move of the dialogue must be made to a participant of the dialogue…, and the agents take it in turns to receive moves…)
4.2, (Terminology that allows us to talk about the relationship between two dialogues: ‘Sub-dialogue of’…, ‘top-level dialogue’…, ‘top-dialogue of’…, and ‘extends’…)
4.3, Let D be a dialogue with participants x1 and x2 such that topic(D) = gamma. We say that m(s)… is a matched-closed for D iff m(s-1) = (P, close, gamma) and m(s) = (~P, close, gamma).
So a matched-close will terminate a dialogue D but only if D has not already terminated and any sub-dialogues that are embedded within D have already terminated.
4.4, Let D be a dialogue. D terminates at t iff the following conditions hold…
4.5, The current dialogue is… (the innermost dialogue that has not yet terminated).
We adopt the standard approach of associating a commitment store with each agent participating in a dialogue. A commitment store is a set of beliefs that the agent has asserted so far in the course of the dialogue. As commitment stores consist of things that the agent has already publicly declared, its contents are visible to the other agent participating in the dialogue. For this reason, when constructing an argument, an agent may make use of not only its own beliefs but also those from the other agent’s commitment store.
4.6, A commitment store associated with an agent… is a set of beliefs.
An agent’s commitment store grows monotonically over time. If an agent makes a move asserting an argument, every element of the support is added to the agent’s commitment store. This is the only time the commitment store is updated.
4.7, Commitment store update…
… when an argument inquiry dialogue with topic ‘alpha1 ^ … ^ alphaN -> phi’ is opened, a question store associated with that dialogue is created whose contents are {alpha1, …, alphaN}. Throughout the dialogue the participant agents will both try to provide arguments for the literals in the question store. This may lead them to open further nested argument inquiry dialogues that have a topic a rule consequent is a literal in the question store.
4.8… a question store… is a finite set of literals such that…
A protocol is a function that returns the set of moves that are legal for an agent to make at a particular point in a particular type of dialogue…
4.9, The argument inquiry protocol is a function (that takes the top-level dialogue that the agents are participating in and the identifier of the agent whose turn it is to move, and returns the set of legal moves that the agent can make)…
(An agent can only assert an argument or open a rule for a conclusion that is in the current Question Store, and such that the move has not been made by either agent at an earlier timepoint in the dialogue.)
Note that it is straightforward to check conformance with the protocol as the protocol only refers to public elements of the dialogue.
… a specific strategy function… allows an agent to select exactly one legal move to make at each timepoint in an argument inquiry dialogue. A strategy is personal to an agent and the move that it returns depends on the agent’s private beliefs. The argument inquiry strategy states that if there are any legal moves that assert an argument that can be constructed by the agent (by means of its belief base and the other agent’s commitment store) then a single one of those moves is selected…, else if there are any legal open moves with a defeasible rule as their content that is in the agent’s beliefs then a single one of these moves is selected… If there are no such moves then a close move is made.
4.10… The function pickO returns the chosen open move…
4.11… The function pickA returns the chosen assert move…
4.12, The argument inquiry strategy is a function (that takes the top-level dialogue that the agents are participating in and the identifier of the agent whose turn it is to move, and returns exactly one of the legal moves)…
Note that a top-level argument inquiry dialogue will always have a defeasible fact as its topic, but each of its sub-dialogues will always have a defeasible rule as its topic.
4.13, D is a well-formed argument inquiry dialogue iff… (D does not continue after it has terminated and is generated by the argument inquiry strategy).
… Note that we assume some higher-level planning component that guides the agent when deciding whether to enter into a dialogue, who this dialogue should be with and on what topic, i.e. that makes the decision to make the move m1.
15.1-15.3, A Generative Inquiry Dialogue System
Notes taken from ‘A Generative Inquiry Dialogue System’ (2007), by Elizabeth Black and Anthony Hunter
“… We focus on inquiry dialogues that allow two agents to share knowledge in order to construct an argument for a specific claim…”
1, Introduction
Dialogue games are now a common approach to defining communicative agent behaviour, especially when this behaviour is argumentation-based… Dialogue games are normally made up of a set of communicative acts called moves, a set of rules that state which moves it is legal to make at any point in a dialogue (the protocol), a set of rules that define the effect of making a move, and a set of rules that determine when a dialogue terminates. Most of the work so far has looked at modelling different types of dialogue in the Walton and Krabbe typology… here we provide a generative system.
... A key contribution of this work is that we not only provide a protocol for modelling inquiry dialogues but we also provide a specific strategy to be followed, making this system sufficient to also generate inquiry dialogues… and this allows us to consider soundness and completeness properties of our system.
2, Motivation
Our work has been motivated by the medical domain. Argumentation allows us to deal with the incomplete, inconsistent and uncertain knowledge that is characteristic of medical knowledge. There are often many different healthcare professionals involved in the care of a patient, each of whom has a particular type of specialised knowledge and who must cooperate in order to provide the best possible care for the patient…
Inquiry dialogues are a type of knowledge that would be of particular use in the healthcare domain, where it is often the case that people have distinct types of knowledge and so need to interact with others in order to have all the information necessary to make a decision…
… We compare the outcome of our dialogues with the outcome that would be arrived at by a single agent that has at its beliefs the union of both the agents participating in the dialogues beliefs. This is, in some sense, the ideal situation, where there are no constraints on the sharing of beliefs.
3, Knowledge Representation and Arguments
We adapt Garcia and Simari’s Defeasible Logic Programming (DeLP)… for representing each agent’s beliefs…
The presentation in this section differs slightly from that in (Garcia and Simari’s DeLP)… as (they) assume a set of strict rules, which we assume to be empty, and they assume facts to be non-defeasible. We assume that all knowledge is defeasible due to the nature of medical knowledge, which is constantly expanding…
3.1, A defeasible rule is denoted 'alpha1 ^ … ^ alphaN -> alpha0' where alphai is a literal… A defeasible fact is denoted 'alpha' where alpha is a literal. A belief is either a defeasible rule of a defeasible fact.
3.2, A belief base associated with an agent x is a finite set…
3.3… A defeasible derivation of (a literal) ‘alpha’ from (a set of beliefs)… is a finite sequence alpha1, alpha2, …, alphaN of literals such that alphaN is alpha and each literal… is in the sequence because…
3.4, An argument constructed from a set of, possibly inconsistent, beliefs… is a minimally consistent set from which the claim can be defeasibly derived…
“… We focus on inquiry dialogues that allow two agents to share knowledge in order to construct an argument for a specific claim…”
1, Introduction
Dialogue games are now a common approach to defining communicative agent behaviour, especially when this behaviour is argumentation-based… Dialogue games are normally made up of a set of communicative acts called moves, a set of rules that state which moves it is legal to make at any point in a dialogue (the protocol), a set of rules that define the effect of making a move, and a set of rules that determine when a dialogue terminates. Most of the work so far has looked at modelling different types of dialogue in the Walton and Krabbe typology… here we provide a generative system.
... A key contribution of this work is that we not only provide a protocol for modelling inquiry dialogues but we also provide a specific strategy to be followed, making this system sufficient to also generate inquiry dialogues… and this allows us to consider soundness and completeness properties of our system.
2, Motivation
Our work has been motivated by the medical domain. Argumentation allows us to deal with the incomplete, inconsistent and uncertain knowledge that is characteristic of medical knowledge. There are often many different healthcare professionals involved in the care of a patient, each of whom has a particular type of specialised knowledge and who must cooperate in order to provide the best possible care for the patient…
Inquiry dialogues are a type of knowledge that would be of particular use in the healthcare domain, where it is often the case that people have distinct types of knowledge and so need to interact with others in order to have all the information necessary to make a decision…
… We compare the outcome of our dialogues with the outcome that would be arrived at by a single agent that has at its beliefs the union of both the agents participating in the dialogues beliefs. This is, in some sense, the ideal situation, where there are no constraints on the sharing of beliefs.
3, Knowledge Representation and Arguments
We adapt Garcia and Simari’s Defeasible Logic Programming (DeLP)… for representing each agent’s beliefs…
The presentation in this section differs slightly from that in (Garcia and Simari’s DeLP)… as (they) assume a set of strict rules, which we assume to be empty, and they assume facts to be non-defeasible. We assume that all knowledge is defeasible due to the nature of medical knowledge, which is constantly expanding…
3.1, A defeasible rule is denoted 'alpha1 ^ … ^ alphaN -> alpha0' where alphai is a literal… A defeasible fact is denoted 'alpha' where alpha is a literal. A belief is either a defeasible rule of a defeasible fact.
3.2, A belief base associated with an agent x is a finite set…
3.3… A defeasible derivation of (a literal) ‘alpha’ from (a set of beliefs)… is a finite sequence alpha1, alpha2, …, alphaN of literals such that alphaN is alpha and each literal… is in the sequence because…
3.4, An argument constructed from a set of, possibly inconsistent, beliefs… is a minimally consistent set from which the claim can be defeasibly derived…
Friday, 30 March 2007
Why don't the agents just pool together all their beliefs?
Quote taken from the last paragraph of section 4 of 'A Generative Inquiry Dialogue System' by Elizabeth Black and Anthony Hunter
In our simple example, it seems that it would be more straightforward to pool both agents beliefs and apply a reasoning procedure to this set of beliefs. However, given a real-world scenario this would not necessarily be the case. When dealing with the medical domain we have to consider privacy issues that would restrict agents from simply pooling all beliefs. It is also sometimes the case that agents have vast belief bases and the communication cost involved in sharing all beliefs would be prohibitive.
In our simple example, it seems that it would be more straightforward to pool both agents beliefs and apply a reasoning procedure to this set of beliefs. However, given a real-world scenario this would not necessarily be the case. When dealing with the medical domain we have to consider privacy issues that would restrict agents from simply pooling all beliefs. It is also sometimes the case that agents have vast belief bases and the communication cost involved in sharing all beliefs would be prohibitive.
Thursday, 29 March 2007
What is an Inquiry Dialogue?
Paragraph taken from the introduction of 'A Generative Inquiry Dialogue System' by Elizabeth Black and Anthony Hunter (2007)
In this paper we focus on inquiry dialogues. Walton and Krabbe define an inquiry dialogue as arising from an initial situation of "general ignorance" and as having the main goal to achieve the "growth of knowledge and agreement". Each indiviual participating in an inquiry dialogue has the goal to "find a 'proof' or destroy one" ('Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning', page 66)... we have defined two different types of inquiry dialogue, each of which we believe fits the general definition:
- warrant inquiry dialogue - the 'proof' takes the form of a dialectical tree (essentially a tree with an argument at each node, whose arcs represent the counter-argument relation and that has at its root an argument whose claim is the topic of the dialogue).
- argument inquiry dialogue - the 'proof' takes the form of an argument for the topic of the dialogue.
Argument inquiry dialogues are commonly embedded in warrant inquiry dialogues. In this paper, we will focus only on argument inquiry dialogues.
In this paper we focus on inquiry dialogues. Walton and Krabbe define an inquiry dialogue as arising from an initial situation of "general ignorance" and as having the main goal to achieve the "growth of knowledge and agreement". Each indiviual participating in an inquiry dialogue has the goal to "find a 'proof' or destroy one" ('Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning', page 66)... we have defined two different types of inquiry dialogue, each of which we believe fits the general definition:
- warrant inquiry dialogue - the 'proof' takes the form of a dialectical tree (essentially a tree with an argument at each node, whose arcs represent the counter-argument relation and that has at its root an argument whose claim is the topic of the dialogue).
- argument inquiry dialogue - the 'proof' takes the form of an argument for the topic of the dialogue.
Argument inquiry dialogues are commonly embedded in warrant inquiry dialogues. In this paper, we will focus only on argument inquiry dialogues.
Wednesday, 28 March 2007
13.4-13.5, Computing ideal sceptical argumentation
Notes taken from ‘Computing ideal sceptical argumentation’ by P. M. Dung, Paolo Mancarella and F. Toni (2006)
4, Computing ideal beliefs for assumption-based argumentation
… Our proof procedure for computing ideal beliefs for assumption-based frameworks is defined in terms IB-dispute derivations, adapted from (a variant of) the dispute derivations of the paper ‘Dialectic proof procedures for assumption-based, admissible argumentation’ for computing admissible beliefs, that we refer to here as AB-dispute derivations…
By virtue of relying upon potential attacks, dispute derivations thus actually construct concrete dispute trees, that may correspond to one, no or multiple dispute trees.
Note that all our dispute derivations will be of finite length. This is because our ultimate goal is to develop effective proof procedures that can be used to support practical applications.
Computing admissible beliefs
The efficient construction of admissible dispute trees for assumption-based argumentation frameworks can be obtained via AB-dispute derivations… These are variants of the dispute derivations of ‘Dialectic proof procedures for assumption-based, admissible argumentation’, that improve upon them by being “more complete”… GB-dispute derivations (which compute grounded beliefs) can be seen as an initial step between dispute trees and the actual, final form of AB-dispute derivations, in that they are correct, but highly incomplete and inefficient…
4.1, Let ABF be an assumption-based argumentation framework, and AF be the corresponding abstract framework. Given a dispute tree T for AF,
- for any opponent node labelled by an argument ‘b’ with child a proponent node labelled by an argument ‘a’ if ‘a’ attacks some assumption ‘alpha’ in the set supporting ‘b’ then ‘alpha’ is said to be the culprit in ‘b’;
- the set of all assumptions supporting the arguments in the defence set of T is referred to as the assumption-defence set of T.
(Theorem 4.1) … Given a dispute tree T for AF, T is admissible iff no culprit in the argument of an opponent node belongs to the assumption-defence set of T.
In GB-dispute derivations:
- the set of culprits Ci is used to filter potential defence arguments…
- the set of defence assumptions Ai is used to filter potential culprits…
so that the final assumption-defence set constructed by the derivation does not attack itself (theorem 4.1).
4.2… Given a selection function, a GB-dispute derivation of a defence set A for a sentence ‘alpha’ is a finite sequence of quadruples (P0, O0, A0, C0), …, (Pi, Oi, A, Ci), …, (Pn, On, An, Cn) where…
(Theorem 4.2) Given a GB-dispute derivation of a defence set A for a sentence ‘alpha’:
- A is admissible and it is contained in the grounded set of assumptions;
- There exists A’ (a subset of A) and an argument A’ |- alpha.
Note that GB-dispute derivations succeed in many cases where other procedures for computing grounded beliefs fail. However, GB-dispute derivations are “highly incomplete” for admissibility, in that they fail to compute admissible sets in many cases, corresponding to infinite dispute trees.
AB-dispute derivations incorporate a filtering by defence assumptions so that they can (finitely) compute infinite admissible dispute trees… Moreover, AB-dispute derivations incorporate a filtering by culprit assumptions so that they can be more efficient…
4.3… Given a selection function, a AB-dispute derivation of a defence set A for a sentence ‘alpha’ is a finite sequence of quadruples (P0, O0, A0, C0), …, (Pi, Oi, A, Ci), …, (Pn, On, An, Cn) where…
(Theorem 4.3) For every AB-dispute derivation of a defence set A for a sentence ‘alpha’, the defence set A is admissible, and there exists some A’ (a subset of A) that supports an argument for ‘alpha’.
4.4, An assumption-based framework AF is positively acyclic (or p-acyclic for short) if the dependency graph of AF+ is acyclic. (AF+ is the framework obtained by deleting all assumptions appearing in the premises of the inference rules of R.)
(Lemma 4.1) Given an assumption based framework, let an infinite partial deduction be an infinite sequence of steps defined as in Definition 2.4. Given a p-acyclic framework, there exists no infinite partial deduction.
Computing ideal beliefs
… Like AB-dispute derivations, IB-dispute derivations are sequences of tuples, but these tuples are of the form (Pi, Oi, Ai, Ci, Fi). Fi a novel component intuitively holding all potential attacks against the proponent: by virtue of theorem 3.3 IB-dispute derivations need to make sure that no admissible set of assumptions containing any attack in Fi exists. This check is ultimately performed by a new kind of (subsidiary) dispute derivations, that we call Fail dispute derivations…
(Notation 4.2) Let S be a set of sentences in L. By Fail(S) we mean that there exists no admissible set E of assumptions such that E ||- S.
IB-dispute derivations are sequences of tuples of the form (Pi, Oi, Ai, Ci, Fi) where
- the new component Fi holds all multisets S for which we want to prove that Fail(S) (these are the potential attacks S dealt with in step 2 of AB-dispute derivation)
- Pi, Oi, Ai, Ci are as in AB-dispute derivations, except that sentences occurring in the multisets in Oi may be marked.
Intuitively, IB-dispute derivations compute an admissible support for the given sentence ‘alpha’ while trying to check that no admissible set attacks it. As soon as a (potential) attack is found, this is stored in the F component of the tuple to check that this fails to be become/admissible. Whenever a potential culprit is ignored in a potential attack, this is marked so that it will not be selected again. Selected elements in the potential attacks in the O component are chosen amongst the unmarked elements. Thus, we will impose that, given a multisets S in Oi, the selection function will only select unmarked sentences in Su. (Su is the set of unmarked sentences in S.)
4.5… Given a selection function, an IB-dispute derivation of an ideal support A for a sentence alpha is a finite sequences of tuples (P0, O0, A0, C0, F0), …, (Pi, Oi, A, Ci, Fi), …, (Pn, On, An, Cn, Fn) where…
(Theorem 4.5) If there exists an IB-dispute derivation for ‘alpha’, then ‘alpha’ is an ideal belief.
(Theorem 4.6) Given a p-acyclic framework with an underlying finite language, if ‘alpha’ is an ideal belief then there exists an IB-dispute derivation for ‘alpha’.
4.6… Given a selection function, a Fail-dispute derivation of a multiset of sentences S is a sequence D0, …, Dn such that each Di is a set of quadruples of the form (P, O, A, C) where…
(Theorem 4.7) If there exists a Fail-dispute derivation for a multiset of sentences S then Fail(S) holds.
(Corollary 4.2) If there exists an IB-dispute derivation for ‘alpha’ in which Fail-dispute derivations are used to check whether Fail holds, then ‘alpha’ is an ideal belief (i.e. the derivations are sound).
Fail-dispute derivations are complete if AB-dispute derivations are complete for the admissibility semantics. Thus:
(Theorem 4.8) For p-acyclic frameworks with a finite underlying language, if there exists no admissible argument supporting S then there is a Fail-dispute derivation for S.
(Corollary 4.3) For p-acyclic frameworks with a finite underlying language, IB-dispute derivations in which Fail-dispute derivations are used to check Fail, are complete.
5, Conclusion…
4, Computing ideal beliefs for assumption-based argumentation
… Our proof procedure for computing ideal beliefs for assumption-based frameworks is defined in terms IB-dispute derivations, adapted from (a variant of) the dispute derivations of the paper ‘Dialectic proof procedures for assumption-based, admissible argumentation’ for computing admissible beliefs, that we refer to here as AB-dispute derivations…
By virtue of relying upon potential attacks, dispute derivations thus actually construct concrete dispute trees, that may correspond to one, no or multiple dispute trees.
Note that all our dispute derivations will be of finite length. This is because our ultimate goal is to develop effective proof procedures that can be used to support practical applications.
Computing admissible beliefs
The efficient construction of admissible dispute trees for assumption-based argumentation frameworks can be obtained via AB-dispute derivations… These are variants of the dispute derivations of ‘Dialectic proof procedures for assumption-based, admissible argumentation’, that improve upon them by being “more complete”… GB-dispute derivations (which compute grounded beliefs) can be seen as an initial step between dispute trees and the actual, final form of AB-dispute derivations, in that they are correct, but highly incomplete and inefficient…
4.1, Let ABF be an assumption-based argumentation framework, and AF be the corresponding abstract framework. Given a dispute tree T for AF,
- for any opponent node labelled by an argument ‘b’ with child a proponent node labelled by an argument ‘a’ if ‘a’ attacks some assumption ‘alpha’ in the set supporting ‘b’ then ‘alpha’ is said to be the culprit in ‘b’;
- the set of all assumptions supporting the arguments in the defence set of T is referred to as the assumption-defence set of T.
(Theorem 4.1) … Given a dispute tree T for AF, T is admissible iff no culprit in the argument of an opponent node belongs to the assumption-defence set of T.
In GB-dispute derivations:
- the set of culprits Ci is used to filter potential defence arguments…
- the set of defence assumptions Ai is used to filter potential culprits…
so that the final assumption-defence set constructed by the derivation does not attack itself (theorem 4.1).
4.2… Given a selection function, a GB-dispute derivation of a defence set A for a sentence ‘alpha’ is a finite sequence of quadruples (P0, O0, A0, C0), …, (Pi, Oi, A, Ci), …, (Pn, On, An, Cn) where…
(Theorem 4.2) Given a GB-dispute derivation of a defence set A for a sentence ‘alpha’:
- A is admissible and it is contained in the grounded set of assumptions;
- There exists A’ (a subset of A) and an argument A’ |- alpha.
Note that GB-dispute derivations succeed in many cases where other procedures for computing grounded beliefs fail. However, GB-dispute derivations are “highly incomplete” for admissibility, in that they fail to compute admissible sets in many cases, corresponding to infinite dispute trees.
AB-dispute derivations incorporate a filtering by defence assumptions so that they can (finitely) compute infinite admissible dispute trees… Moreover, AB-dispute derivations incorporate a filtering by culprit assumptions so that they can be more efficient…
4.3… Given a selection function, a AB-dispute derivation of a defence set A for a sentence ‘alpha’ is a finite sequence of quadruples (P0, O0, A0, C0), …, (Pi, Oi, A, Ci), …, (Pn, On, An, Cn) where…
(Theorem 4.3) For every AB-dispute derivation of a defence set A for a sentence ‘alpha’, the defence set A is admissible, and there exists some A’ (a subset of A) that supports an argument for ‘alpha’.
4.4, An assumption-based framework AF is positively acyclic (or p-acyclic for short) if the dependency graph of AF+ is acyclic. (AF+ is the framework obtained by deleting all assumptions appearing in the premises of the inference rules of R.)
(Lemma 4.1) Given an assumption based framework, let an infinite partial deduction be an infinite sequence of steps defined as in Definition 2.4. Given a p-acyclic framework, there exists no infinite partial deduction.
Computing ideal beliefs
… Like AB-dispute derivations, IB-dispute derivations are sequences of tuples, but these tuples are of the form (Pi, Oi, Ai, Ci, Fi). Fi a novel component intuitively holding all potential attacks against the proponent: by virtue of theorem 3.3 IB-dispute derivations need to make sure that no admissible set of assumptions containing any attack in Fi exists. This check is ultimately performed by a new kind of (subsidiary) dispute derivations, that we call Fail dispute derivations…
(Notation 4.2) Let S be a set of sentences in L. By Fail(S) we mean that there exists no admissible set E of assumptions such that E ||- S.
IB-dispute derivations are sequences of tuples of the form (Pi, Oi, Ai, Ci, Fi) where
- the new component Fi holds all multisets S for which we want to prove that Fail(S) (these are the potential attacks S dealt with in step 2 of AB-dispute derivation)
- Pi, Oi, Ai, Ci are as in AB-dispute derivations, except that sentences occurring in the multisets in Oi may be marked.
Intuitively, IB-dispute derivations compute an admissible support for the given sentence ‘alpha’ while trying to check that no admissible set attacks it. As soon as a (potential) attack is found, this is stored in the F component of the tuple to check that this fails to be become/admissible. Whenever a potential culprit is ignored in a potential attack, this is marked so that it will not be selected again. Selected elements in the potential attacks in the O component are chosen amongst the unmarked elements. Thus, we will impose that, given a multisets S in Oi, the selection function will only select unmarked sentences in Su. (Su is the set of unmarked sentences in S.)
4.5… Given a selection function, an IB-dispute derivation of an ideal support A for a sentence alpha is a finite sequences of tuples (P0, O0, A0, C0, F0), …, (Pi, Oi, A, Ci, Fi), …, (Pn, On, An, Cn, Fn) where…
(Theorem 4.5) If there exists an IB-dispute derivation for ‘alpha’, then ‘alpha’ is an ideal belief.
(Theorem 4.6) Given a p-acyclic framework with an underlying finite language, if ‘alpha’ is an ideal belief then there exists an IB-dispute derivation for ‘alpha’.
4.6… Given a selection function, a Fail-dispute derivation of a multiset of sentences S is a sequence D0, …, Dn such that each Di is a set of quadruples of the form (P, O, A, C) where…
(Theorem 4.7) If there exists a Fail-dispute derivation for a multiset of sentences S then Fail(S) holds.
(Corollary 4.2) If there exists an IB-dispute derivation for ‘alpha’ in which Fail-dispute derivations are used to check whether Fail holds, then ‘alpha’ is an ideal belief (i.e. the derivations are sound).
Fail-dispute derivations are complete if AB-dispute derivations are complete for the admissibility semantics. Thus:
(Theorem 4.8) For p-acyclic frameworks with a finite underlying language, if there exists no admissible argument supporting S then there is a Fail-dispute derivation for S.
(Corollary 4.3) For p-acyclic frameworks with a finite underlying language, IB-dispute derivations in which Fail-dispute derivations are used to check Fail, are complete.
5, Conclusion…
Making a set of inference rules "proper"
Given this set of inference rules:
p <- a, b
~a <- ~a
~b <-
s <- ~p
where the set of candidate assumptions is {a, b, ~p}
In trying to make this set of rules "proper" by taking into account the finer details, I came up with this:
p <- a, b
not_a <- not_a, c
not_b <- d
s <- e
where
the set of candidate assumptions is {a, b, c, d, e}
and the contrary relations are
~a = {not_a}, ~b = {not_b}, ~c = {a}, ~d = {b}, ~e = {p}
Is this correct? In particular, I'm not sure whether the rule 'not_a <- not_a, c'
captures the loop of '~a <- ~a', and whether the contrary of 'c' should be {a} or
something else.
You have introduced far too many elements in your translation, it would have been sufficient to say:
p <- a, b
~a <- ~a
~b <-
s <- ~p
where {a,b,~p} are assumptions with contraries ~a, ~b, p respectively.
Please do not forget that the underlying deductive system can be anything, and the only requirement on assumptions is that they do not occur as conclusions of rules, so the above is a perfectly legitimate assumption-based framework that makes our point.
If you would like to avoid the use of ~ (which is fine), you could have
p <- a, b
not_a <- not_a
not_b<-
s <- not_p
where {a,b,not_p} are assumptions with contraries not_a, not_b, p respectively.
You can see that the only difference with the above is purely syntactic.
p <- a, b
~a <- ~a
~b <-
s <- ~p
where the set of candidate assumptions is {a, b, ~p}
In trying to make this set of rules "proper" by taking into account the finer details, I came up with this:
p <- a, b
not_a <- not_a, c
not_b <- d
s <- e
where
the set of candidate assumptions is {a, b, c, d, e}
and the contrary relations are
~a = {not_a}, ~b = {not_b}, ~c = {a}, ~d = {b}, ~e = {p}
Is this correct? In particular, I'm not sure whether the rule 'not_a <- not_a, c'
captures the loop of '~a <- ~a', and whether the contrary of 'c' should be {a} or
something else.
You have introduced far too many elements in your translation, it would have been sufficient to say:
p <- a, b
~a <- ~a
~b <-
s <- ~p
where {a,b,~p} are assumptions with contraries ~a, ~b, p respectively.
Please do not forget that the underlying deductive system can be anything, and the only requirement on assumptions is that they do not occur as conclusions of rules, so the above is a perfectly legitimate assumption-based framework that makes our point.
If you would like to avoid the use of ~ (which is fine), you could have
p <- a, b
not_a <- not_a
not_b<-
s <- not_p
where {a,b,not_p} are assumptions with contraries not_a, not_b, p respectively.
You can see that the only difference with the above is purely syntactic.
Subscribe to:
Posts (Atom)