Search engine for discovering works of Art, research articles, and books related to Art and Culture
Javascript must be enabled to continue!
Intuitionistic ancestral logic
View through CrossRef
Abstract
In this article we define pure intuitionistic Ancestral Logic ( iAL ), extending pure intuitionistic First-Order Logic ( iFOL ). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL given by its realizer for the transitive closure, TC . We derive this operator from the natural type theoretic definition of TC using intersection. We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further show that iAL subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes. We also extract schemes from proofs that iAL specifications are solvable.
Title: Intuitionistic ancestral logic
Description:
Abstract
In this article we define pure intuitionistic Ancestral Logic ( iAL ), extending pure intuitionistic First-Order Logic ( iFOL ).
This logic is a dependently typed abstract programming language with computational functionality beyond iFOL given by its realizer for the transitive closure, TC .
We derive this operator from the natural type theoretic definition of TC using intersection.
We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory.
We further show that iAL subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes.
We also extract schemes from proofs that iAL specifications are solvable.
Related Results
Epistemic extensions of substructural inquisitive logics
Epistemic extensions of substructural inquisitive logics
Abstract
In this paper, we study the epistemic extensions of distributive substructural inquisitive logics. Substructural inquisitive logics are logics of questions ...
A Logic for Desire Based on Causal Inference
A Logic for Desire Based on Causal Inference
Abstract
Reasoning about desire plays a significant role in logic, artificial intelligence and philosophy, etc. In this paper, we propose an interpretation of desire...
Masculinity and Conversion in Old English Guthlac A
Masculinity and Conversion in Old English Guthlac A
The article turns to Judith Butler’s writings on abjection to elucidate the Christian subjectivity that emerges from the Old English poetic life of Guthlac of Crowland, known as Gu...
The challenge of sustaining organizational hybridity: The role of power and agency
The challenge of sustaining organizational hybridity: The role of power and agency
Hybrid organizations harbor different and often conflicting institutional logics, thus facing the challenge of sustaining their hybridity. Crucial to overcoming this challenge is t...
Bridge Principles and Epistemic Norms
Bridge Principles and Epistemic Norms
AbstractIs logic normative for belief? A standard approach to answering this question has been to investigate bridge principles relating claims of logical consequence to norms for ...
Slow Fire: Serial Thinking and Hardy's Genres of Induction
Slow Fire: Serial Thinking and Hardy's Genres of Induction
This essay considers the use of “serial thinking”—an approach to representation and cognition that emphasizes repetition, enumeration, and aggregation—in the work of Thomas Hardy. ...
Dynamic epistemic logics for abstract argumentation
Dynamic epistemic logics for abstract argumentation
AbstractThis paper introduces a multi-agent dynamic epistemic logic for abstract argumentation. Its main motivation is to build a general framework for modelling the dynamics of a ...
Limit ultrapowers and abstract logics
Limit ultrapowers and abstract logics
AbstractWe associate with any abstract logic L a family F(L) consisting, intuitively, of the limit ultrapowers which are complete extensions in the sense of L.For every countably g...