Discrete mathematics is the study of mathematical structures that can be considered "discrete" rather than "continuous". Objects studied in discrete mathematics include integers, graphs, and statements in logic. By contrast, discrete mathematics excludes topics in "continuous mathematics" such as real numbers, calculus or Euclidean geometry. Discrete objects can often be enumerated by integers; more formally, discrete mathematics has been characterized as the branch of mathematics dealing with countable sets. However, there is no exact definition of the term "discrete mathematics".
A relational database is a database based on the relational model of data, as proposed by E. F. Codd in 1970. A system used to maintain relational databases is a relational database management system (RDBMS). Many relational database systems are equipped with the option of using the SQL for querying and maintaining the database.
In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
In computer science, Backus–Naur form or Backus normal form (BNF) is a metasyntax notation for context-free grammars, often used to describe the syntax of languages used in computing, such as computer programming languages, document formats, instruction sets and communication protocols. It is applied wherever exact descriptions of languages are needed: for instance, in official language specifications, in manuals, and in textbooks on programming language theory.
In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
The Knuth–Bendix completion algorithm is a semi-decision algorithm for transforming a set of equations into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra.
OBJ is a programming language family introduced by Joseph Goguen in 1976, and further worked on by Jose Meseguer.
In computer science, graph transformation, or graph rewriting, concerns the technique of creating a new graph out of an original graph algorithmically. It has numerous applications, ranging from software engineering to layout algorithms and picture generation.
In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.
In mathematics, computer science and logic, overlap, as a property of the reduction rules in term rewriting system, describes a situation where a number of different reduction rules specify potentially contradictory ways of reducing a reducible expression, also known as a redex, within a term.
The Abstract Rewriting Machine (ARM) is a virtual machine which implements term rewriting for minimal term rewriting systems.
John Vivian Tucker is a British computer scientist and expert on computability theory, also known as recursion theory. Computability theory is about what can and cannot be computed by people and machines. His work has focused on generalising the classical theory to deal with all forms of discrete/digital and continuous/analogue data; and on using the generalisations as formal methods for system design; based on abstract data types and on the interface between algorithms and physical equipment.
In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact.
The following outline is provided as an overview of and topical guide to formal science:
In computer science, algebraic semantics is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program specifications in a formal manner.
In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.
Patrick Denis Lincoln is an American computer scientist leading the Computer Science Laboratory (CSL) at SRI International. Educated at MIT and then Stanford, he joined SRI in 1989 and became director of the CSL around 1998. He previously held positions with ETA Systems, Los Alamos National Laboratory, and MCC.
In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules. They were both proved inconsistent by Jean-Yves Girard in 1972. This result led to the realization that Martin-Löf's original 1971 type theory was inconsistent as it allowed the same "Type in Type" behaviour that Girard's paradox exploits.
José Meseguer is a Spanish computer scientist, and professor at the University of Illinois at Urbana–Champaign. He leads the university's Formal Methods and Declarative Languages Laboratory.
