ピーター・B・アンドリュース

ピーター・ブルース・アンドリュース（1937年11月1日 - 2025年4月21日）^{[ 6 ]}はアメリカの数学論理学者である。彼は数学論理Q0_の創始者である。また、包帯を完全に外すことなく傷口にアクセスできる包帯システムの特許も取得している。^{[ 7 ]}

彼の研究グループは、一階述語論理および高階述語論理のための自動定理証明システムであるTPS ^{[ 8 ]}を設計した。TPSのサブシステムETPSは、対話的に自然演繹証明を構築することで学生が論理を学ぶのを支援するために使用されている。TPSのソースコードはインターネットアーカイブで入手可能である。^{[ 9 ]}

リストは彼の個人ウェブページで入手可能です。^{[ 10 ]}

• Andrews, Peter B. (1965).型変数を用いた超限型理論. North Holland Publishing Company, Amsterdam.
• Andrews, Peter B. (1971). 「型理論における分解」. Journal of Symbolic Logic 36 , 414–432.
• Andrews, Peter B. (1981). 「一般的な組み合わせによる定理証明」. J. Assoc. Comput. 3月28日、第2号、193–214頁。
• アンドリュース、ピーター・B. (1986).数理論理学と型理論入門：証明を通して真理へ. コンピュータ科学と応用数学. ISBN 978-0-1205-8535-9アカデミック・プレス社、フロリダ州オーランド。
• Andrews, Peter B. (1989). 「接続と高階論理について」. J. Automat. Reason. 5 , no. 3, 257–291.
• Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Fr​​ank ; Xi, Hongwei (1996). "TPS: 古典型理論のための定理証明システム". J. Automat. Reason. 16 , no. 3, 321–353.
• アンドリュース、ピーター・B. (2002).数理論理学と型理論入門：証明を通して真理へ. 第2版. 応用論理学シリーズ、27. ISBN 978-1-4020-0763-7クルーワー・アカデミック・パブリッシャーズ、ドルトレヒト。