William Scott, Stephen Cook, Joseph Kasser
Abstract. Requirements form the basis of the systems engineering life cycle activities but creating a good set of requirements is a difficult task. Some difficulties can be reduced through the...
Computing over the reals: Foundations for scientific computing (2008)
The problems of scientific computing often arise from the study of continuous processes, and questions of computability and complexity over the reals are of central importance in laying the...
Computing over the reals: Foundations for scientific computing (2008)
We give a detailed treatment of the “bit-model ” of computability and complexity of real functions and subsets of R n, and argue that this is a good way to formalize many problems of scientific...
We prove the following results: (i) PV proves NP ⊆ P/poly iff PV proves coNP ⊆ NP/O(1). (ii) If PV proves NP ⊆ P/poly then PV proves that the Polynomial Hierarchy collapses to the Boolean...
Comments and Corrections Appreciated (2008)
Almost-Complete draft (450 pages) now available on our web sites.
Initial HOWTO Submission (2007)
Automatic Speech Recognition (ASR) on Linux is becoming easier. Several packages are available for users as well as developers. This document describes the basics of speech recognition and describes...
Relating the Provable Collapse of P to NC¹ and the Power of Logical Theories (2007)
. We show that the following three statements are equivalent: QPV is conservative over QALV, QALV proves its open induction formulas, and QALV proves P=NC 1 . Here QPV and QALV are first order...
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
Stephen Cook, Russell Impagliazzo, Tomoyuki Yamakami
2 We show that any two complexity classes satisfying some general conditions are distinct relative to a generic oracle iff the corresponding type-2 classes are distinct. 3 1
Validation of Extended Transition Networks Using (2007)
Gedblog I, Stephen Cook, Patrizia Asirelli, Keith Jeffery, Ox Qx
In order to prove properties of information systems, we need a formalism for representing the system, a set of construction rules for the appropriate class of system, and a suitable environment for...
The Strength of Replacement in Weak (2007)
Arithmetic Stephen Cook, Stephen Cook, Neil Thapen, Thus In S, Unconditionally That V
The replacement (or collection or choice) axiom scheme BB() asserts bounded quanti er exchange as follows: 8i< jaj 9x<a(i;x) ! 9w 8i< jaj (i; [w] i ) where is in the class of formulas. The...
The Importance of the P versus NP Question (2007)
found. There are potential counterexamples to this assertion, most famously the deep results of Robertson and Seymour [RS95]. They prove that every minor closed family of graphs can be recognized in...
Funding provided by the European Union, grant ADVISOR (IST-1999-11287). (2007)
Steve Maybank, Tugdual Le Bou#ant, Tugdual Le Bou#ant, Nils T Siebel, Nils T Siebel, Stephen Cook, ...
1
Email: We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is...
Challenges of Highly Adaptable Information Systems (2007)
Stephen Cook Rachel, Stephen Cook, Rachel Harrison, Timothy Millea, Lily Sun
this paper has identified
A Second-Order System for Polytime Reasoning (2007)
Based On Gr, Stephen Cook, Antonina Kolokolova, Consequences Of S
We introduce a second-order system V 1 -Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Gradel's (Gradel, 1992) second-order Horn characterization of P. Our system...
The Complexity of Proving Discrete Jordan Curve Theorem (2007)
The Jordan Curve Theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under...
Relativizing Small Complexity Classes and their Theories (2007)
Klaus Aehlig, Stephen Cook, Phuong Nguyen
Existing definitions of the relativizations of NC 1, L and NL do not preserve the inclusions NC 1 ⊆ L, NL ⊆ AC 1. We start by giving the first definitions that preserve them. Here for L and NL we...
Relativizing Small Complexity Classes and their Theories (2007)
Klaus Aehlig, Stephen Cook, Phuong Nguyen
Abstract. Existing definitions of the relativizations of NC 1, L and NL do not preserve the inclusions NC 1 ⊆ L, NL ⊆ AC 1. We start by giving the first definitions that preserve them. Here for L...
Relativizing Small Complexity Classes and their Theories (2007)
Klaus Aehlig, Stephen Cook, Phuong Nguyen
Existing definitions of the relativizations of NC 1, L and NL do not preserve the inclusions NC 1 ⊆ L, NL ⊆ AC 1. We start by giving the first definitions that preserve them. Here for L and NL we...
Evolution in software systems: foundations of the SPE classification scheme. (2006)
Lehman, Meir M., Wernick, Paul, Harrison, Rachel, Cook, Stephen
This paper re-examines the SPE taxonomy of evolving software systems, first proposed in 1980 (Lehman). It builds on the concept that software evolution is related to generic theories of evolution. A...
Evolution in software systems: foundations of the SPE classification scheme. (2006)
Lehman, Meir M., Wernick, Paul, Harrison, Rachel, Cook, Stephen
This paper re-examines the SPE taxonomy of evolving software systems, first proposed in 1980 (Lehman). It builds on the concept that software evolution is related to generic theories of evolution. A...
Development of a foundation for military network science - Report prepared for DSTO (2006)
Lawson, Errol Charles, Ferris, Timothy L J, Cropley, David H, Cook, Stephen
Development of a foundation for military network science - Report prepared for DSTO (2006)
Lawson, Errol Charles, Ferris, Timothy L J, Cropley, David H, Cook, Stephen
Theory for TC 0 and Other Small Complexity Classes (2005)
Abstract We present a general method for introducing finitely axiomatizable "minimal " second-order theories for various subclasses of P. We show that our theory VTC 0 for the...
Theories for complexity classes and their propositional translations (2004)
We present in a uniform manner simple two-sorted theories corresponding to each of eight complexity classes between AC 0 and P. We present simple translations between these theories and systems of...
Quantified Propositional Calculus and a Second-Order Theory for NC¹ (2004)
Stephen Cook, Tsuyoshi Morioka
Let H be a proof system for the quantified propositional calculus (QPC). We j -witnessing problem for H to be: given a prenex S j -formula A, an H-proof of A, and a truth assignment to the free...
Quantified Propositional Calculus and aSecond-Order Theory for NC1 (2004)
Stephen Cook, Tsuyoshi Morioka
Abstract Let H be a proof system for the quantified propositional calculus (QPC). Wedefine the \Sigma q j-witnessing problem for H to be: given a prenex \Sigma qj-formula A, anH-proof of A, and a...
A second-order system for polytime reasoning based on Grädel’s theorem (2003)
Stephen Cook, Antonina Kolokolova
Gradel's theorem
A second-order system for polytime reasoning based on Grädel’s theorem (2003)
Stephen Cook, Antonina Kolokolova
Gradel's theorem
A second-order system for polytime reasoning based on Grädel’s theorem (2003)
Stephen Cook, Antonina Kolokolova
Gradel's theorem
Latitudinal and Longitudinal Process Diversity (2003)
Nils T Siebel, Stephen Cook, Manoranjan Satpathy, Daniel Rodríguez
Computation Define Abstract Computing Platform Assess Impact of Exogenous Analyse Non-functional Requirements Deploy Release Generic Software Change Process Figure 1. Software process model,...
The Proof Complexity of Linear Algebra (2003)
We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is...
Review of COTS software integration and T and E techniques from a NATO perspective (2002)
Collignon, Stephane, Cook, Stephen
The use of COTS software products in Defence is an established fact and there is no provision to return to bespoke legacy systems. The use of COTS software, however, can present problems when...
The proof complexity of linear algebra (2002)
We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is...
Cyclosporin monitoring in Australasia: 2002 update of consensus guidelines (2002)
Morris, Raymond G., Ilett, Kenneth F., Tett, Susan E., Ray, John E., Fullinfaw, Robert O., Cooke, Russell, ...
Therapeutic drug monitoring of cyclosporin (CsA) has been established as part of the routine clinical treatment of patients following organ transplantation for more than 20 years, and based on...
Review of COTS software integration and T and E techniques from a NATO perspective (2002)
Collignon, Stephane, Cook, Stephen
The use of COTS software products in Defence is an established fact and there is no provision to return to bespoke legacy systems. The use of COTS software, however, can present problems when...
An initial application of AP-233 (2002)
Scott, William, Cook, Stephen, Harris, David, Smith, John, Johnson, Julian
The System Engineering Design Methodologies (SEDM) project is concerned with potential avenues to exploit the AP-233 system engineering data exchange standard. The project is a joint venture between...
An initial application of AP-233 (2002)
Scott, William, Cook, Stephen, Harris, David, Smith, John, Johnson, Julian
The System Engineering Design Methodologies (SEDM) project is concerned with potential avenues to exploit the AP-233 system engineering data exchange standard. The project is a joint venture between...
Review of COTS software integration and T and E techniques from a NATO perspective (2002)
Collignon, Stephane, Cook, Stephen
The use of COTS software products in Defence is an established fact and there is no provision to return to bespoke legacy systems. The use of COTS software, however, can present problems when...
Rex Gregory, Paul Eason, Jamire Williams, Max Vaclavik, Stephen Cook, Rob Seible, ...
www.governor.state.tx.us/music
The P versus NP problem (2000)
The P versus NP problem is to determine whether every language accepted by some nondeterministic algorithm in polynomial time is also accepted by some (deterministic) algorithm in polynomial time. To...
The P versus NP Problem (2000)
subset L of \Sigma . Each Turing machine M has an associated input alphabet \Sigma. For each string w in \Sigma there is a computation associated with M with input w. (The notions of Turing machine...
The P versus NP problem (2000)
The P versus NP problem is to determine whether every language accepted by some nondeterministic algorithm in polynomial time is also accepted by some (deterministic) algorithm in polynomial time. To...
Bulletin of the Section of Logic (1999)
Volume Pp Stephen, Stephen Cook, Michael Soltys
We introduce the notion of Boolean programs, which provide more concise descriptions of Boolean functions than Boolean circuits. We characterize nonuniform PSPACE in terms of polynomial size families...
The Relative Complexity of NP Search Problems (1998)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
A systems thinking approach to selecting systems methodologies for defence high-level systems (1998)
A systems thinking approach to selecting systems methodologies for defence high-level systems (1998)
The Relative Complexity of NP Search Problems (1997)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
An Exponential Lower Bound for the Size of Monotone Real Circuits (1997)
We prove a lower bound, exponential in the eighth root of the input length, on the size of monotone arithmetic circuits that solve an NP problem related to clique detection. The result is more...
Managing Heterogeneity in Inter-Operating Medical Information Systems (1996)
Maurice Dixon, Jana Kohoutková, Stephen Cook, Keith Jeffery, Brian Read
This paper reports the progress made in managing the heterogeneities that arise in interoperating medical information systems. The approach taken is to define a domain ontology through the use of a...
An Exponential Lower Bound for the Size of Monotone Real Circuits (1995)
Armin Haken Stephen, Stephen Cook
We prove a lower bound, exponential in the eighth root of the input length, on the size of monotone arithmetic circuits that solve an NP problem related to clique detection. The result is more...
The Relative Complexity of NP Search Problems (1995)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
The Relative Complexity of NP Search Problems (1995)
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, Toniann Pitassi
Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems. Many interesting search problems not known...
Functional interpretations of feasibly constructive arithmetic (1993)
Stephen Cook, Alasdair Urquhart
i
A new recursion-theoretic characterization of the polytime functions (1992)
Stephen Bellantoni, Stephen Cook
Abstract. We give a recursion-theoretic characterization of FP which describes polynomial time computation independently of any externally imposed resource bounds. In particular, this syntactic...
The Recognition of Deterministic CFL's in Small Time and Space (1983)
Von Braunmühl, Burchard, Cook, Stephen, Mehlhorn, Kurt, Verbeek, Rutger
Let S(n) be a nice space bound such that log2 n S(n) n. Then every DCFL is recognized by a multitape Turing machine simultaneously in time O(n2/S(n)) and space O(S(n)), and this time bound is...