Related Research Articles
In mathematical analysis, the intermediate value theorem states that if is a continuous function whose domain contains the interval [a, b], then it takes on any given value between and at some point within the interval.
In computational complexity theory, the class NC (for "Nick's Class") is the set of decision problems decidable in polylogarithmic time on a parallel computer with a polynomial number of processors. In other words, a problem with input size n is in NC if there exist constants c and k such that it can be solved in time O((log n)c) using O(nk) parallel processors. Stephen Cook coined the name "Nick's class" after Nick Pippenger, who had done extensive research on circuits with polylogarithmic depth and polynomial size.
In topology, Urysohn's lemma is a lemma that states that a topological space is normal if and only if any two disjoint closed subsets can be separated by a continuous function.
Zorn's lemma, also known as the Kuratowski–Zorn lemma, is a proposition of set theory. It states that a partially ordered set containing upper bounds for every chain necessarily contains at least one maximal element.
In mathematics, Hilbert's Nullstellensatz is a theorem that establishes a fundamental relationship between geometry and algebra. This relationship is the basis of algebraic geometry. It relates algebraic sets to ideals in polynomial rings over algebraically closed fields. This relationship was discovered by David Hilbert, who proved the Nullstellensatz in his second major paper on invariant theory in 1893.
The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As a Logic for Computable Functions (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.
In mathematics, the uniform boundedness principle or Banach–Steinhaus theorem is one of the fundamental results in functional analysis. Together with the Hahn–Banach theorem and the open mapping theorem, it is considered one of the cornerstones of the field. In its basic form, it asserts that for a family of continuous linear operators whose domain is a Banach space, pointwise boundedness is equivalent to uniform boundedness in operator norm.
In computational complexity theory, a complexity class is a set of computational problems "of related resource-based complexity". The two most commonly analyzed resources are time and memory.
In functional analysis and related branches of mathematics, the Banach–Alaoglu theorem states that the closed unit ball of the dual space of a normed vector space is compact in the weak* topology. A common proof identifies the unit ball with the weak-* topology as a closed subset of a product of compact sets with the product topology. As a consequence of Tychonoff's theorem, this product, and hence the unit ball within, is compact.
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.
The Larch family of formal specification languages are intended for the precise specification of computing systems. They allow the clean specification of computer programs and the formulation of proofs about program behavior.
In theoretical computer science and mathematical logic a string rewriting system (SRS), historically called a semi-Thue system, is a rewriting system over strings from a alphabet. Given a binary relation between fixed strings over the alphabet, called rewrite rules, denoted by , an SRS extends the rewriting relation to all strings in which the left- and right-hand side of the rules appear as substrings, that is , where , , , and are strings.
A Dynkin system, named after Eugene Dynkin, is a collection of subsets of another universal set satisfying a set of axioms weaker than those of 𝜎-algebra. Dynkin systems are sometimes referred to as 𝜆-systems or d-system. These set families have applications in measure theory and probability.
In complexity theory, the Karp–Lipton theorem states that if the Boolean satisfiability problem (SAT) can be solved by Boolean circuits with a polynomial number of logic gates, then
In mathematics, particularly topology, the tube lemma, also called Wallace's theorem, is a useful tool in order to prove that the finite product of compact spaces is compact.
In geometry, the hyperplane separation theorem is a theorem about disjoint convex sets in n-dimensional Euclidean space. There are several rather similar versions. In one version of the theorem, if both these sets are closed and at least one of them is compact, then there is a hyperplane in between them and even two parallel hyperplanes in between them separated by a gap. In another version, if both disjoint convex sets are open, then there is a hyperplane in between them, but not necessarily any gap. An axis which is orthogonal to a separating hyperplane is a separating axis, because the orthogonal projections of the convex bodies onto the axis are disjoint.
John Vogel Guttag is an American computer scientist, professor, and former head of the department of electrical engineering and computer science at MIT. He conducts research on computer networks and medical applications of AI as co-lead of the MIT Computer Science and Artificial Intelligence Laboratory's Networks and Mobile Systems Group.
Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.
In arithmetic combinatorics, the corners theorem states that for every , for large enough , any set of at least points in the grid contains a corner, i.e., a triple of points of the form with . It was first proved by Miklós Ajtai and Endre Szemerédi in 1974 using Szemerédi's theorem. In 2003, József Solymosi gave a short proof using the triangle removal lemma.
In the mathematical field of set theory, an ultrafilter on a set is a maximal filter on the set In other words, it is a collection of subsets of that satisfies the definition of a filter on and that is maximal with respect to inclusion, in the sense that there does not exist a strictly larger collection of subsets of that is also a filter. Equivalently, an ultrafilter on the set can also be characterized as a filter on with the property that for every subset of either or its complement belongs to the ultrafilter.
References
- ↑ 1985 Larch survey, Çarnegie Mellon University
- ↑ John V. Guttag and James Horning with S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing, Larch: Languages and Tools for Formal Specification, Springer-Verlag Texts and Monographs in Computer Science, 1993. ISBN 978-1-4612-2704-5.
- ↑ Pierre Lescanne and "Computer experiments with the REVE term rewriting system generator," Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '83, Austin, Texas, Association for Computing Machinery, New York, NY, pages 99–108.
- ↑ Randy Forgaard and John Guttag, "REVE: a term rewriting system generator with a failure-resistant Knuth-Bendix", Proceedings of a Workshop on Term Rewriting, edited by D. Kapur and D. Musser, April 1984, pages 5–31.