Now showing items 1-12 of 12

• #### Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations ﻿

(Cornell University, 2004-03-26)
In Smullyan's classic book, First-Order Logic, the notion of a Boolean valuation is central in motivating his analytical tableau proof system. Smullyan shows that these valuations are unique if they exist, and then he ...
• #### Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus ﻿

(Cornell University, 2006-12-12)
We prove constructively that for any propositional formula $\phi$ in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of $\phi$ showing that it is ...
• #### FDL: A Prototype Formal Digital Library ﻿

(Cornell University, 2004-06-16)
This manual describes the first prototype of a new kind of system which we call a Formal Digital Library (FDL). We designed the system and assembled the prototype as part of a research project sponsored by the Office of ...
• #### Generating event logics with higher-order processes as realizers ﻿

(2011-08-25)
Our topic is broadening a practical ”proofs-as-programs” method of program development to “proofs-as-processes”. We extend our previous results that implement proofs-as-processes for the standard model of asynchronous ...
• #### A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics ﻿

(Cornell University, 2006-01-30)
As the amount of online formal mathematical content grows, for example through active efforts such as the Mathweb [21], MOWGLI [4], Formal Digital Library, or FDL [1], and others, it becomes increasingly valuable to find ...
• #### The Horus and Ensemble Projects: Accomplishments and Limitations ﻿

(Cornell University, 1999-10)
The Horus and Ensemble efforts culminated a multi-year Cornell research program in process group communication used for fault-tolerance, security and adaptation. Our intent was to understand the degree to which a single ...
• #### Intuitionistic Completeness of First-Order Logic ﻿

(2011-10-07)
We establish completeness for intuitionistic first-order logic, iFOL, showing that is a formula is provable if and only if it is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics ...
• #### Investigating correct-by-construction attack-tolerant systems ﻿

(2011-09-12)
Attack-tolerant distributed systems change their protocols on-the-fly in response to apparent attacks from the environment; they substitute functionally equivalent versions possibly more resistant to detected threats. ...
• #### The Logic of Events, a framework to reason about distributed systems ﻿

(2012 Languages for Distributed Algorithms (LADA) workshop, 2012-01-23)
• #### A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics. ﻿

(Cornell University, 2003-02-03)
We describe a link between the Nuprl and PVS proof systems that enables users to access PVS from the Nuprl theorem proving environment, to import PVS theories into the Nuprl library, and to browse both Nuprl and PVS ...
• #### Transforming the Academy: Knowledge Formation in the Age of Digital Information ﻿

(Cornell University, 2005-02-08)
Computer-mediated knowledge formation will profoundly change every academic discipline and pose fundamental challenges to the mission of the modern research university in teaching the new knowledge, securing sound methods ...
• #### The Triumph of Types: Principia Mathematica's Impact on Computer Science ﻿

(2011-07-16)
Types now play an essential role in computer science; their ascent originates from Principia Mathematica. Type checking and type inference algorithms are used to prevent semantic errors in programs, and type theories are ...