default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMichael Beeson
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2022
[j22]Michael Beeson
, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe:
Larry Wos: Visions of Automated Reasoning. J. Autom. Reason. 66(4): 439-461 (2022)- [j21]Michael Beeson:
Euclid after Computer Proof-Checking. Am. Math. Mon. 129(7): 623-646 (2022) - 2020
- [i4]Michael Beeson:
On the Notion of Equal Figures in Euclid. CoRR abs/2008.12643 (2020)
2010 – 2019
- 2019
- [j20]Michael Beeson, Julien Narboux, Freek Wiedijk:
Proof-checking Euclid. Ann. Math. Artif. Intell. 85(2-4): 213-257 (2019) - 2017
- [j19]Michael Beeson, Larry Wos:
Finding Proofs in Tarskian Geometry. J. Autom. Reason. 58(1): 181-207 (2017) - [i3]Michael Beeson, Julien Narboux, Freek Wiedijk:
Proof-checking Euclid. CoRR abs/1710.00787 (2017) - 2016
- [j18]Michael Beeson:
Constructive Geometry and the Parallel postulate. Bull. Symb. Log. 22(1): 1-104 (2016) - [j17]Michael Beeson:
Mixing Computations and Proofs. J. Formaliz. Reason. 9(1): 71-99 (2016) - [i2]Michael Beeson, Larry Wos:
Finding Proofs in Tarskian Geometry. CoRR abs/1606.07095 (2016) - 2015
- [j16]Michael Beeson:
A constructive version of Tarski's geometry. Ann. Pure Appl. Log. 166(11): 1199-1273 (2015) - [j15]Michael Beeson, Pierre Boutry, Julien Narboux:
Herbrand's Theorem and non-Euclidean Geometry. Bull. Symb. Log. 21(2): 111-122 (2015) - 2014
- [c12]Michael Beeson, Larry Wos:
OTTER Proofs in Tarskian Geometry. IJCAR 2014: 495-510 - 2012
- [c11]Michael Beeson:
Proof and Computation in Geometry. Automated Deduction in Geometry 2012: 1-30 - [c10]Michael Beeson:
Logic of Ruler and Compass Constructions. CiE 2012: 46-55 - 2011
- [c9]Michael Beeson, Jay Halcomb, Wolfgang Mayer:
Inconsistencies in the Process Specification Language (PSL). ATE 2011: 9-19
2000 – 2009
- 2006
- [j14]Michael Beeson:
Mathematical Induction in Otter-Lambda. J. Autom. Reason. 36(4): 311-344 (2006) - [j13]Michael Beeson:
A Tour through Mathematical Logic by Robert S. Wolf. Am. Math. Mon. 113(3): 275-280 (2006) - [p3]Michael Beeson, William McCune:
Otter/Ivy. The Seventeen Provers of the World 2006: 36-40 - 2005
- [j12]Michael Beeson, Freek Wiedijk:
The meaning of infinity in calculus and computer algebra systems. J. Symb. Comput. 39(5): 523-538 (2005) - [j11]Michael Beeson, Robert Veroff, Larry Wos:
Double-Negation Elimination in Some Propositional Logics. Stud Logica 80(2-3): 195-234 (2005) - 2004
- [c8]Michael Beeson:
Lambda Logic. IJCAR 2004: 460-474 - 2003
- [i1]Michael Beeson, Robert Veroff, Larry Wos:
Double-Negation Elimination in Some Propositional Logics. CoRR cs.LO/0301026 (2003) - 2002
- [c7]Michael Beeson, Freek Wiedijk:
The Meaning of Infinity in Calculus and Computer Algebra Systems. AISC 2002: 246-258 - 2001
- [j10]Michael Beeson:
Automatic Derivation of the Irrationality of e. J. Symb. Comput. 32(4): 333-349 (2001) - [c6]Michael Beeson:
A Second-Order Theorem Prover Applied to Circumscription. IJCAR 2001: 318-324
1990 – 1999
- 1999
- [c5]Michael Beeson:
Automatic derivation of the irrationality of e. Calculemus 1999: 420-439 - 1998
- [c4]Michael Beeson:
Automatic Generation of Epsilon-Delta Proofs of Continuity. AISC 1998: 67-83 - [c3]Michael Beeson:
Unification in Lambda-Calculi with if-then-else. CADE 1998: 103-118 - [p2]Michael Beeson:
Design principles of Mathpert: software to support education in algebra and calculus. Computer-Human Interaction in Symbolic Computation 1998: 163-177 - [p1]Michael Beeson:
Erratum to: Algorithm animation with Agat. Computer-Human Interaction in Symbolic Computation 1998: 209 - 1995
- [j9]Michael Beeson:
Using Nonstandard Analysis to Ensure the Correctness of Symbolic Computations. Int. J. Found. Comput. Sci. 6(3): 299-338 (1995) - 1992
- [c2]Michael Beeson:
Mathpert: Computer Support for Learning Algebra, Trig, and Calculus. LPAR 1992: 454-456
1980 – 1989
- 1989
- [c1]Michael Beeson:
Some Applications of Gentzen's Proof Theory in Automated Deduction. ELP 1989: 101-156 - 1988
- [j8]Michael Beeson:
Towards a Computation System Based on Set Theory. Theor. Comput. Sci. 60: 297-340 (1988) - 1984
- [j7]Michael Beeson, Andre Scedrov:
Church's Thesis, Continuity, and Set Theory. J. Symb. Log. 49(2): 630-643 (1984) - 1982
- [j6]Michael Beeson:
Recursive models for constructive set theories. Ann. Math. Log. 23(2-3): 127-178 (1982)
1970 – 1979
- 1978
- [j5]Michael Beeson:
A Type-Free Godel Interpretation. J. Symb. Log. 43(2): 213-227 (1978) - [j4]Michael Beeson:
Some Relations Between Classical and Constructive Mathematics. J. Symb. Log. 43(2): 228-246 (1978) - 1976
- [j3]Michael Beeson:
The Unprovability in Intuitionistic Formal Systems of the Continuity of Effective Operations on the Reals. J. Symb. Log. 41(1): 18-24 (1976) - [j2]Michael Beeson:
Derived Rules of Inference Related to the Continuity of Effective Operations. J. Symb. Log. 41(2): 328-336 (1976) - 1975
- [j1]Michael Beeson:
The Nonderivability in Intuitionistic Formal Systems of Theorems on the Continuity of Effective Operations. J. Symb. Log. 40(3): 321-346 (1975)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 22:47 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
