Jean Gallier

Last updated

Jean Henri Gallier (born 1949) is a researcher in computational logic at the University of Pennsylvania, where he holds appointments in the Computer and Information Science Department and the Department of Mathematics.

Contents

Biography

Gallier was born January 5, 1949, in Nancy, France, and holds dual French and American citizenship. He earned his baccalauréat at the Lycée de Sèvres in 1966, and a degree in civil engineering at the École Nationale des Ponts et Chaussées in 1972. [1] He then moved to the University of California, Los Angeles for his graduate studies, earning a Ph.D. in computer science in 1978 under the joint supervision of Sheila Greibach and Emily Perlinski Friedman. His dissertation was entitled Semantics and Correctness of Classes of Deterministic and Nondeterministic Recursive Programs. [1] [2] After postdoctoral study at the University of California, Santa Barbara, he joined the University of Pennsylvania Department of Computer and Information Science in 1978. At Pennsylvania, he was promoted to full professor in 1990, gained a secondary appointment to the Department of Mathematics in 1994, and directed the French Institute of Culture and Technology from 2001 to 2004. [1]

Contributions

Gallier's most heavily cited research paper, with his student William F. Dowling, gives a linear time algorithm for Horn-satisfiability. [DG84] This is a variant of the Boolean satisfiability problem: its input is a Boolean formula in conjunctive normal form with at most one positive literal per clause, and the goal is to assign truth values to the variables of the formula to make the whole formula true. Solving Horn-satisfiability problems is the central computational paradigm in the Prolog programming language. [3]

Gallier is also the author of five books in computational logic, [G86] computational geometry, [G99] [G00] low-dimensional topology, [GX13] and discrete mathematics. [G11]

Selected publications

Research papers

Books

Related Research Articles

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

<span class="mw-page-title-main">Discrete mathematics</span> Study of discrete mathematical structures

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".

In mathematics and computer science, the Entscheidungsproblem is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms.

In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or a cluster concept. As a normal form, it is useful in automated theorem proving.

In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form which gives it useful properties for use in logic programming, formal specification, and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.

In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time.

In computational complexity theory, the Cook–Levin theorem, also known as Cook's theorem, states that the Boolean satisfiability problem is NP-complete. That is, it is in NP, and any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the Boolean satisfiability problem.

In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn-satisfiability and Horn clauses are named after Alfred Horn.

Geometric modeling is a branch of applied mathematics and computational geometry that studies methods and algorithms for the mathematical description of shapes. The shapes studied in geometric modeling are mostly two- or three-dimensional, although many of its tools and principles can be applied to sets of any finite dimension. Today most geometric modeling is done with computers and for computer-based applications. Two-dimensional models are important in computer typography and technical drawing. Three-dimensional models are central to computer-aided design and manufacturing (CAD/CAM), and widely used in many applied technical fields such as civil and mechanical engineering, architecture, geology and medical image processing.

In computational complexity, problems that are in the complexity class NP but are neither in the class P nor NP-complete are called NP-intermediate, and the class of such problems is called NPI. Ladner's theorem, shown in 1975 by Richard E. Ladner, is a result asserting that, if P ≠ NP, then NPI is not empty; that is, NP contains problems that are neither in P nor NP-complete. Since it is also true that if NPI problems exist, then P ≠ NP, it follows that P = NP if and only if NPI is empty.

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

<span class="mw-page-title-main">Harry R. Lewis</span> American computer scientist

Harry Roy Lewis is an American computer scientist, mathe­ma­ti­cian, and uni­ver­sity admin­i­stra­tor known for his research in com­pu­ta­tional logic, textbooks in theoretical computer science, and writings on computing, higher education, and technology. He is Gordon McKay Research Professor of Computer Science at Harvard University, and was Dean of Harvard College from 1995 to 2003.

In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi-Elgot-Trakhtenbrot theorem gives a logical characterization of the regular languages.

In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not.

In mathematical logic, computational complexity theory, and computer science, the existential theory of the reals is the set of all true sentences of the form

<span class="mw-page-title-main">Blake canonical form</span> Standard form of Boolean function

In Boolean logic, a formula for a Boolean function f is in Blake canonical form (BCF), also called the complete sum of prime implicants, the complete sum, or the disjunctive prime form, when it is a disjunction of all the prime implicants of f.

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power.

Yilun Dianna Xu is a mathematician and computer scientist whose research concerns the computational geometry of curves and surfaces, computer vision, and computer graphics. She is a professor of computer science at Bryn Mawr College where she chairs the computer science department.

References

  1. 1 2 3 Curriculum vitae, retrieved 2017-03-26.
  2. ↑ Jean Gallier at the Mathematics Genealogy Project
  3. ↑ Dechter, Rina (2003), Constraint Processing, The Morgan Kaufmann Series in Artificial Intelligence, San Francisco, CA: Morgan Kaufmann, p. 307, ISBN   9781558608900 .
  4. ↑ Pfenning, Frank (1989), "Review: Jean H. Gallier, Logic for Computer Science. Foundations of Automatic Theorem Proving" (PDF), Journal of Symbolic Logic, 54 (1): 288–289, doi:10.2307/2275035, JSTOR   2275035, S2CID   117298919 .
  5. ↑ Kallay, Michael (2001), Review of Curves and surfaces in geometric modeling, MR 1823812.
  6. ↑ Jüttler, Bert (2001), Review of Geometric methods and applications, MR 1792535. Updated for 2nd ed., 2012, MR 2663906.
  7. ↑ Williams, Hugh (November 2002), "Geometric Methods and Applications for Computer Science and Engineering", The Mathematical Gazette, 86 (507): 564, doi:10.2307/3621198, JSTOR   3621198 .
  8. ↑ Hunacek, Mark (2011), Review of Geometric methods and applications, Mathematical Association of America.
  9. ↑ Pinter, Gabriella (2012), Review of Discrete Mathematics, Mathematical Association of America.
  10. ↑ Löh, Clara, Review of A guide to the classification theorem for compact surfaces, MR 3026641.
  11. ↑ Wood, Bill (2014), Review of A Guide to the Classification Theorem for Compact Surfaces, Mathematical Association of America.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.