References of "Fuenmayor, David"
     in
Bookmark and Share    
Peer Reviewed
See detailA Computational-Hermeneutic Approach for Conceptual Explicitation
Fuenmayor, David; Benzmüller, Christoph UL

in Nepomuceno, A.; Magnani, L.; Salguero, F. (Eds.) et al Model-Based Reasoning in Science and Technology -- Inferential Models for Logic, Language, Cognition and Computation (2019)

We present a computer-supported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for ... [more ▼]

We present a computer-supported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for higher-order logics and aims at formalizing natural-language argumentative discourse using flexible combinations of expressive non-classical logics. In doing so, it allows us to render explicit the tacit conceptualizations implicit in argumentative discursive practices. Our approach operates on networks of structured arguments and is iterative and two-layered. At one layer we search for logically correct formalizations for each of the individual arguments. At the next layer we select among those correct formalizations the ones which honor the argument’s dialectic role, i.e. attacking or supporting other arguments as intended. We operate at these two layers in parallel and continuously rate sentences’ formalizations by using, primarily, inferential adequacy criteria. An interpretive, logical theory will thus gradually evolve. This theory is composed of meaning postulates serving as explications for concepts playing a role in the analyzed arguments. Such a recursive, iterative approach to interpretation does justice to the inherent circularity of understanding: the whole is understood compositionally on the basis of its parts, while each part is understood only in the context of the whole (hermeneutic circle). We summarily discuss previous work on exemplary applications of human-in-the-loop computational hermeneutics in metaphysical discourse. We also discuss some of the main challenges involved in fully-automating our approach. By sketching some design ideas and reviewing relevant technologies, we argue for the technological feasibility of a highly-automated computational hermeneutics. [less ▲]

Detailed reference viewed: 142 (0 UL)
Full Text
Peer Reviewed
See detailHarnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories
Fuenmayor, David; Benzmüller, Christoph UL

in Nayak, A.; Sharma, A. (Eds.) PRICAI 2019: Trends in Artificial Intelligence (2019, August 23)

Detailed reference viewed: 74 (0 UL)
Full Text
See detailCan Computers Help to Sharpen our Understanding of Ontological Arguments?
Benzmüller, Christoph UL; Fuenmayor, David

in Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science Spiritual Quest, 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India (2018)

Detailed reference viewed: 32 (0 UL)
Full Text
Peer Reviewed
See detailFormalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
Fuenmayor, David; Benzmüller, Christoph UL

in Archive of Formal Proofs (2018)

An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has ... [more ▼]

An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence. [less ▲]

Detailed reference viewed: 56 (0 UL)
Full Text
Peer Reviewed
See detailA Case Study On Computational Hermeneutics: E. J. Lowe's Modal Ontological Argument
Fuenmayor, David; Benzmüller, Christoph UL

in IfCoLog Journal of Logics and Their Applications (2018), 5(7), 1567-1603

Computers may help us to better understand (not just verify) arguments. In this article we defend this claim by showcasing the application of a new, computer-assisted interpretive method to an exemplary ... [more ▼]

Computers may help us to better understand (not just verify) arguments. In this article we defend this claim by showcasing the application of a new, computer-assisted interpretive method to an exemplary natural-language argument with strong ties to metaphysics and religion: E. J. Lowe’s modern variant of St. Anselm’s ontological argument for the existence of God. Our new method, which we call computational hermeneutics, has been particularly conceived for use in interactive-automated proof assistants. It aims at shedding light on the meanings of words and sentences by framing their inferential role in a given argument. By employing automated theorem reasoning technology within interactive proof assistants, we are able to drastically reduce (by several orders of magnitude) the time needed to test the logical validity of an argument’s formalization. As a result, a new approach to logical analysis, inspired by Donald Davidson’s account of radical interpretation, has been enabled. In computational hermeneutics, the utilization of automated reasoning tools effectively boosts our capacity to expose the assumptions we indirectly commit ourselves to every time we engage in rational argumentation and it fosters the explicitation and revision of our concepts and commitments. [less ▲]

Detailed reference viewed: 58 (0 UL)
Full Text
Peer Reviewed
See detailComputational Hermeneutics: Using Computers to Interpret Philosophical Arguments (Abstract)
Fuenmayor, David; Benzmüller, Christoph UL

in Logical Correctness, Workshop at UNILOG'2018, UNILOG'2018 Book of Abstracts (2018)

Detailed reference viewed: 35 (0 UL)
Full Text
Peer Reviewed
See detailComputer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
Benzmüller, Christoph UL; Fuenmayor, David

in Archive of Formal Proofs (2017)

Computers may help us to understand --not just verify-- philosophical arguments. By utilizing modern proof assistants in an iterative interpretive process, we can reconstruct and assess an argument by ... [more ▼]

Computers may help us to understand --not just verify-- philosophical arguments. By utilizing modern proof assistants in an iterative interpretive process, we can reconstruct and assess an argument by fully formal means. Through the mechanization of a variant of St. Anselm's ontological argument by E. J. Lowe, which is a paradigmatic example of a natural-language argument with strong ties to metaphysics and religion, we offer an ideal showcase for our computer-assisted interpretive method. [less ▲]

Detailed reference viewed: 48 (1 UL)
Full Text
Peer Reviewed
See detailAutomating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
Fuenmayor, David; Benzmüller, Christoph UL

in KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI (2017, September)

A shallow semantic embedding of an intensional higher-order modal logic (IHOML) in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in ... [more ▼]

A shallow semantic embedding of an intensional higher-order modal logic (IHOML) in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in his textbook Types, Tableaus and Gödel’s God in order to discuss his emendation of Gödel’s ontological argument for the existence of God. Utilizing IHOML, the most interesting parts of Fitting’s textbook are formalized, automated and verified in the Isabelle/HOL proof assistant. A particular focus thereby is on three variants of the ontological argument which avoid the modal collapse, which is a strongly criticized side-effect in Gödel’s resp. Scott’s original work. [less ▲]

Detailed reference viewed: 84 (6 UL)
Full Text
Peer Reviewed
See detailTypes, Tableaus and Gödel's God in Isabelle/HOL
Fuenmayor, David; Benzmüller, Christoph UL

in Archive of Formal Proofs (2017)

A computer-formalisation of the essential parts of Fitting's textbook "Types, Tableaus and Gödel's God" in Isabelle/HOL is presented. In particular, Fitting's (and Anderson's) variant of the ontological ... [more ▼]

A computer-formalisation of the essential parts of Fitting's textbook "Types, Tableaus and Gödel's God" in Isabelle/HOL is presented. In particular, Fitting's (and Anderson's) variant of the ontological argument is verified and confirmed. This variant avoids the modal collapse, which has been criticised as an undesirable side-effect of Kurt Gödel's (and Dana Scott's) versions of the ontological argument. Fitting's work is employing an intensional higher-order modal logic, which we shallowly embed here in classical higher-order logic. We then utilize the embedded logic for the formalisation of Fitting's argument. (See also the earlier AFP entry ``Gödel's God in Isabelle/HOL''.) [less ▲]

Detailed reference viewed: 45 (2 UL)
Full Text
Peer Reviewed
See detailThe Virtues of Automated Theorem Proving in Metaphysics --- A Case Study: E. J. Lowe's Modal Ontological Argument
Fuenmayor, David; Benzmüller, Christoph UL; Steen, Alexander UL et al

in The 2nd World Congress on Logic and Religion -- Book of Abstracts (2017)

Detailed reference viewed: 50 (2 UL)