November 17, 2015
Argumentation is a vital aspect of intelligent behaviour by humans; it provides the means for comparing conflicting information by analysing pros and cons, or in equivalence, arguments for and against a case when trying to make a decision. A number of frameworks have been proposed for formally defining an argument and relations of attack between arguments. This presentation focuses on argumentation based on classical logic where an argument is defined to be a pair < Φ, α > with Φ being a minimal and consistent set of formulas that classically entails a “claim” formula α1 <#sdfootnote1sym>. The expressivity of classical propositional logic allows for complicated knowledge to be represented but its computational cost is an issue. To this end, automated theorem proving algorithms for producing logical arguments and counterarguments efficiently will be presented in this talk. The solution is based on connection graphs2 <#sdfootnote2sym> and resolution theorem proving. A connection graph is a graph where each node is a clause and each arc denotes there exist complementary disjuncts between nodes. A connection graph allows for a substantially reduced search space to be used when seeking all the arguments for a claim from a given knowledgebase. In addition, its structure provides information on how its nodes can be linked with each other by resolution, providing this way the basis for applying algorithms which search for arguments by traversing the graph. The algorithms presented are based on classical propositional logic with an extension to first-order logic.
1 <#sdfootnote1anc> Besnard, P., & Hunter, A. (2001). A logic-based theory of deductive arguments.*Artificial Intelligence*, *128*(1), 203-235.
2 <#sdfootnote2anc> Kowalski, R. (1975). A proof procedure using connection graphs. *Journal of the ACM (JACM)*, *22*(4), 572-595.