Related Research Articles
Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.
Raymond Merrill Smullyan was an American mathematician, magician, concert pianist, logician, Taoist, and philosopher.
Jan Łukasiewicz was a Polish logician and philosopher who is best known for Polish notation and Łukasiewicz logic. His work centred on philosophical logic, mathematical logic and history of logic. He thought innovatively about traditional propositional logic, the principle of non-contradiction and the law of excluded middle, offering one of the earliest systems of many-valued logic. Contemporary research on Aristotelian logic also builds on innovative works by Łukasiewicz, which applied methods from modern logic to the formalization of Aristotle's syllogistic.
Lehman College is a public college in New York City. Founded in 1931 as the Bronx campus of Hunter College, it became an independent college within CUNY in September 1967. The college is named after Herbert H. Lehman, a former New York governor, United States senator, philanthropist, and the son of Lehman Brothers co-founder Mayer Lehman. It is a senior college of the City University of New York (CUNY) and offers more than 90 undergraduate and graduate degree programs and specializations.
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
Evert Willem Beth was a Dutch philosopher and logician, whose work principally concerned the foundations of mathematics. He was a member of the Significs Group.
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.
Andrzej Wojciech Trybulec was a Polish mathematician and computer scientist noted for work on the Mizar system.
Keith Leonard Clark is an Emeritus Professor in the Department of Computing at Imperial College London, England.
Computational logic is the use of logic to perform or reason about computation. It bears a similar relationship to computer science and engineering as mathematical logic bears to mathematics and as philosophical logic bears to philosophy. It is an alternative rerm for "logic in computer science".
In mathematical logic, a judgment or assertion is a statement or enunciation in a metalanguage. For example, typical judgments in first-order logic would be that a string is a well-formed formula, or that a proposition is true. Similarly, a judgment may assert the occurrence of a free variable in an expression of the object language, or the provability of a proposition. In general, a judgment may be any inductively definable assertion in the metatheory.
Rohit Jivanlal Parikh is an Indian-American mathematician, logician, and philosopher who has worked in many areas in traditional logic, including recursion theory and proof theory. He is a Distinguished Professor at Brooklyn College at the City University of New York (CUNY).
Victor Yakovlevich Pan is a Soviet and American mathematician and computer scientist, known for his research on algorithms for polynomials and matrix multiplication.
John Corcoran was an American logician, philosopher, mathematician, and historian of logic. He is best known for his philosophical work on concepts such as the nature of inference, relations between conditions, argument-deduction-proof distinctions, the relationship between logic and epistemology, and the place of proof theory and model theory in logic. Nine of Corcoran's papers have been translated into Spanish, Portuguese, Persian, and Arabic; his 1989 "signature" essay was translated into three languages. Fourteen of his papers have been reprinted; one was reprinted twice.
Peter William O'Hearn, formerly a research scientist at Meta, is a Distinguished Engineer at Lacework and a Professor of Computer science at University College London (UCL). He has made significant contributions to formal methods for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases.
Sergei Nikolaevich Artemov is a Russian-American researcher in logic and its applications. He currently holds the title of Distinguished Professor at the Graduate Center of the City University of New York where he is the founder and head of its research laboratory for logic and computation. His research interests include proof theory and logic in computer science, optimal control and hybrid systems, automated deduction and verification, epistemology, and epistemic game theory. He is best known for his invention of logics of proofs and justifications.
Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions.
Philippa Anne Gardner is a British computer scientist and academic. She has been Professor of Theoretical Computer Science at the Department of Computing, Imperial College London since 2009. She was director of the Research Institute in Automated Program Analysis and Verification between 2013 and 2016. In 2020 Gardner was elected Fellow of the Royal Academy of Engineering.
Nissim Francez is an Israeli professor, emeritus in the computer science faculty at the Technion, and former head of computational linguistics laboratory in the faculty.
Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.
References
- Fitting, Melvin (1996) [1990]. First-order logic and automated theorem proving (2nd ed.). New York: Springer. doi:10.1007/978-1-4612-2360-3. ISBN 978-1-4612-7515-2.
- Lassez, Jean-Louis; Plotkin, Gordon (1991). Computational Logic — Essays in Honor of Alan Robinson. Cambridge, Massachusetts: MIT Press. ISBN 978-0-262-12156-9.
