Browse ORBi

- What it is and what it isn't
- Green Road / Gold Road?
- Ready to Publish. Now What?
- How can I support the OA movement?
- Where can I learn more?

ORBi

Results 1-14 of 14.
((uid:50001393))
Technical online appendix to "A Structured Argumentation Framework for Modeling Debates in the Formal Sciences" Cramer, Marcos ; Dauphin, Jérémie Report (2018) Detailed reference viewed: 52 (1 UL)Extended Explanatory Argumentation Frameworks Dauphin, Jérémie ; Cramer, Marcos in Theory and Applications of Formal Argumentation (2018) Multiple extensions of Dung's argumentation frameworks (AFs) have been proposed in order to model features of argumentation that cannot be directly modeled in AFs. One technique that has already ... [more ▼] Multiple extensions of Dung's argumentation frameworks (AFs) have been proposed in order to model features of argumentation that cannot be directly modeled in AFs. One technique that has already previously proven useful to study and combine such extensions is the meta-argumentation methodology involving the notion of a flattening. In order to faithfully model the interaction between explanation argumentation in scientific debates, Šešelja and Straßer have introduced Explanatory Argumentation Frameworks (EAFs). In this paper, we first prove that the flattening technique works as expected for recursive (higher-order) attacks. Then we apply this technique in order to combine EAFs with multiple other extensions that have been proposed to AFs, namely with recursive attacks, joint attacks and a support relation between arguments. This gives rise to Extended Explanatory Argumentation Frameworks (EEAFs). We illustrate the applicability of EEAFs by using them to model a piece of argumentation from a research-level philosophy book. [less ▲] Detailed reference viewed: 135 (8 UL)ASPIC-END: Structured Argumentation with Explanations and Natural Deduction Dauphin, Jérémie ; Cramer, Marcos in Theory and Applications of Formal Argumentation (2018) We propose ASPIC-END, an adaptation of the structured argumentation framework ASPIC+ which can incorporate explanations and natural deduction style arguments. We discuss an instantiation of ASPIC-END that ... [more ▼] We propose ASPIC-END, an adaptation of the structured argumentation framework ASPIC+ which can incorporate explanations and natural deduction style arguments. We discuss an instantiation of ASPIC-END that models argumentation about explanations of semantic paradoxes (e.g. the Liar paradox), and we show that ASPIC-END satisfies rationality postulates akin to those satisfied by ASPIC+. [less ▲] Detailed reference viewed: 115 (11 UL)Modelling argumentation on Axiom of Choice in ASPIC-END -- Technical report Cramer, Marcos Report (2017) In this technical report, we present an application of the structured argumentation methodology to a debate in the foundations of mathematics. We work with ASPIC-END, a recently proposed adaptation of the ... [more ▼] In this technical report, we present an application of the structured argumentation methodology to a debate in the foundations of mathematics. We work with ASPIC-END, a recently proposed adaptation of the structured argumentation framework ASPIC+ which can incorporate debates about logical principles, natural deduction style arguments and explanations. We apply this framework to build a preliminary formal model of parts of the debate that mathematicians had about the Axiom of Choice in the early 20th century. Furthermore, we briefly discuss the insight into the strengths and drawbacks of the modeling capacities of ASPIC-END that we have gained from producing this model. [less ▲] Detailed reference viewed: 32 (4 UL)Postulates for Revocation Schemes Cramer, Marcos ; Casini, Giovanni in Cramer, Marcos; Casini, Giovanni (Eds.) Postulates for Revocation Schemes (2017, January 18) In access control frameworks with the possibility of delegating permissions and administrative rights, delegation chains can form. There are di erent ways to treat these delegation chains when revoking ... [more ▼] In access control frameworks with the possibility of delegating permissions and administrative rights, delegation chains can form. There are di erent ways to treat these delegation chains when revoking rights, which give rise to di erent revocation schemes. Hagstr om et al. [11] proposed a framework for classifying revocation schemes, in which the di erent revocation schemes are de ned graph-theoretically. At the outset, we identify multiple problems with Hagstr om et al.'s de nitions of the revocation schemes, which can pose security risks. This paper is centered around the question how one can systematically ensure that improved de nitions of the revocation schemes do not lead to similar problems. For this we propose to apply the axiomatic method originating in social choice theory to revocation schemes. Our use of the axiomatic method resembles its use in belief revision theory. This means that we de ne postulates that describe the desirable behaviour of revocation schemes, study which existing revocation frameworks satisfy which postulates, and show how all de ned postulates can be satis ed by de ning the revocation schemes in a novel way. [less ▲] Detailed reference viewed: 93 (26 UL)Implicit dynamic function introduction and Ackermann-like Function Theory Cramer, Marcos in The IfCoLog Journal of Logics and their Applications (2017) We discuss a feature of the natural language of mathematics – the implicit dynamic introduction of functions – that has, to our knowledge, not been captured in any formal system so far. If this feature is ... [more ▼] We discuss a feature of the natural language of mathematics – the implicit dynamic introduction of functions – that has, to our knowledge, not been captured in any formal system so far. If this feature is used without limitations, it yields a paradox analogous to Russell’s paradox. Hence any formalism capturing it has to impose some limitations on it. We sketch two formalisms, both extensions of Dynamic Predicate Logic, that innovatively do capture this feature, and that differ only in the limitations they impose onto it. One of these systems is based on Ackermann-like Function Theory, a novel foundational theory of functions that is inspired by Ackermann Set Theory and that interprets ZFC. [less ▲] Detailed reference viewed: 36 (1 UL)Kripke Semantics for BL0 and BL – Technical report Cramer, Marcos ; Report (2017) We describe Kripke semantics for the access control logics BL0 and BL, developed by Garg and Pfenning. Detailed reference viewed: 27 (6 UL)The Naproche system: Proof-checking mathematical texts in controlled natural language Cramer, Marcos in Sprache und Datenverarbeitung. International Journal for Language Data Processing (2016), 2014(1-2), 9-33 The Naproche system is a system for linguistically analysing and proof-checking mathematical texts written in a controlled natural language, i.e. a subset of the usual natural language of mathematical ... [more ▼] The Naproche system is a system for linguistically analysing and proof-checking mathematical texts written in a controlled natural language, i.e. a subset of the usual natural language of mathematical texts defined through a formal grammar. This paper gives an overview over the linguistic and logical techniques developed for the Naproche system. Special attention is given to the dynamic nature of quantification in natural language, to the phenomenon of implicit function introduction in mathematical texts, and to the usage of definitions for dynamically extending the language of a mathematical text. [less ▲] Detailed reference viewed: 69 (6 UL)Distributed Autoepistemic Logic and its Application to Access Control ; Cramer, Marcos ; et al in Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (2016) In this paper we define and study an extension of autoepistemic logic (AEL) called distributed autoepistemic logic (dAEL) with multiple agents that have full introspection in their own knowledge as well ... [more ▼] In this paper we define and study an extension of autoepistemic logic (AEL) called distributed autoepistemic logic (dAEL) with multiple agents that have full introspection in their own knowledge as well as in that of others. This mutual full introspection between agents is motivated by an application of dAEL in access control. We define 2- and 3-valued semantic operators for dAEL. Using these operators, approximation fixpoint theory, an abstract algebraic framework that unifies different knowledge representation formalisms, immediately yields us a family of semantics for dAEL, each based on different intuitions that are well-studied in the context of AEL. The application in access control also motivates an extension of dAEL with inductive definitions (dAEL(ID)). We explain a use-case from access control to demonstrate how dAEL(ID) can be fruitfully applied to this domain and discuss how well-suited the different semantics are for the application in access control. [less ▲] Detailed reference viewed: 21 (0 UL)Resilient Delegation Revocation with Precedence for Predecessors is NP-Complete Cramer, Marcos ; ; et al in IEEE 29th Computer Security Foundations Symposium (2016) In ownership-based access control frameworks with the possibility of delegating permissions and administrative rights, chains of delegated accesses will form. There are different ways to treat these ... [more ▼] In ownership-based access control frameworks with the possibility of delegating permissions and administrative rights, chains of delegated accesses will form. There are different ways to treat these delegation chains when revoking rights, which give rise to different revocation schemes. One possibility studied in the literature is to revoke rights by issuing negative authorizations, meant to ensure that the revocation is resilient to a later reissuing of the rights, and to resolve conflicts between principals by giving precedence to predecessors, i.e.\ principals that come earlier in the delegation chain. However, the effects of negative authorizations have been defined differently by different authors. Having identified three definitions of this effect from the literature, the first contribution of this paper is to point out that two of these three definitions pose a security threat. However, avoiding this security threat comes at a price: We prove that with the safe definition of the effect of negative authorizations, deciding whether a principal does have access to a resource is an NP-complete decision problem. We discuss two limitations that can be imposed on an access-control system in order to reduce the complexity of the problem back to a polynomial complexity: Limiting the length of delegation chains to an integer m reduces the runtime complexity of determining access to O(n^m), and requiring that principals form a hierarchy that graph-theoretically forms a rooted tree makes this decision problem solvable in quadratic runtime. Finally we discuss an approach that can mitigate the complexity problem in practice without fully getting rid of NP-completeness. [less ▲] Detailed reference viewed: 16 (0 UL)A logical approach to restricting access in online social networks Cramer, Marcos ; Pang, Jun ; Zhang, Yang in Proceedings of the 20th ACM Symposium on Access Control Models and Technologies (2015) Detailed reference viewed: 65 (8 UL)A Logic of Trust for Reasoning about Delegation and Revocation Cramer, Marcos ; Ambrossio, Diego Agustin ; in Proceedings of the 20th ACM Symposium on Access Control Models and Technologies (2015) Detailed reference viewed: 48 (6 UL)Modelling the usage of partial functions and undefined terms using presupposition theory Cramer, Marcos in Geschke, Stefan; Loewe, Benedikt; Schlicht, Philipp (Eds.) Infinity, Computability and Metamathematics – Festschrift celebrating the 60th birthdays of Peter Koepke and Philip Welch (2014) We describe how the linguistic theory of presuppositions can be used to analyse and model the usage of partial functions and undefined terms in mathematical texts. We compare our account to other accounts ... [more ▼] We describe how the linguistic theory of presuppositions can be used to analyse and model the usage of partial functions and undefined terms in mathematical texts. We compare our account to other accounts of partial functions and undefined terms, showing how our account models the actual usage of partial functions and undefined terms more faithfully than existing accounts. The model described in this paper has been developed for the Naproche system, a computer system for proof-checking mathematical texts written in controlled natural language, and has largely been implemented in this system. [less ▲] Detailed reference viewed: 58 (11 UL)Modelling implicit dynamic introduction of function symbols in mathematical texts Cramer, Marcos in de Paiva, Valeria; et al. (Eds.) Joint Proceedings of the Second Workshop on Natural Language and Computer Science (NLCS’14) & 1st International Workshop on Natural Language Services for Reasoners (NLSR 2014) Affliated to RTA-TLCA, VSL 2014 July 17-18, 2014 Vienna, Austria. (2014) The specialized language of mathematics has a number of linguistically and logically interesting features. One of them, which to our knowledge has not been systematically studied before, is the implicit ... [more ▼] The specialized language of mathematics has a number of linguistically and logically interesting features. One of them, which to our knowledge has not been systematically studied before, is the implicit dynamic introduction of function symbols, exemplified by constructs of the form "for every x there is an f(x) such that ...". We present an extension of Groenendijk and Stokhof's Dynamic Predicate Logic – Typed Higher-Order Dynamic Predicate Logic – which formally models this feature of the language of mathematics. Furthermore, we illustrate how the implicit dynamic introduction of function symbols is treated in the proof checking algorithm of the Naproche system. [less ▲] Detailed reference viewed: 42 (2 UL) |
||