デビッド・プレイステッド

デビッド・アラン・プレイステッドは、ノースカロライナ大学チャペルヒル校のコンピューターサイエンス教授です。

研究分野

プレイステッドの研究分野は、項書き換えシステム自動定理証明論理プログラミングアルゴリズムなどです。定理証明における彼の研究業績には、再帰的経路順序付け、[ 1 ] 結合的経路順序付け、[ 2 ]抽象化、[ 3 ]簡略化および修正された問題簡約形式、[ 4 ] [ 5 ]基底簡約性、[ 6 ] 非標準節形式変換、[ 7 ]剛体E-統一[ 8 ]クヌース・ベンディックス完備[ 9 ] [ 10 ]定理証明における置換規則、[ 11 ]インスタンスベースの定理証明戦略、[ 12 ]定理証明における意味論[ 13 ]に関する研究が含まれます。

教育とキャリア

プレイステッド氏は、1970年にシカゴ大学理学士号、1976年にスタンフォード大学博士号を取得しました。1984年までイリノイ大学アーバナ・シャンペーン校のコンピュータサイエンス学部の教授を務め、その後はノースカロライナ大学チャペルヒル校のコンピュータサイエンス学部の教授を務めています。コンピュータサイエンスに関する出版物を執筆または共著しており、この分野の学者によって引用されています。また、Journal of Symbolic Computation 、Information Processing Letters、Mathematical Systems Theory、Fundamenta Informaticaeなど、多数のプログラム委員会および雑誌の編集委員を務めています。プレイステッド氏は、1982年と1983年にカリフォルニア州メンロパークSRIインターナショナルで長期休暇を過ごしました。また、 1993年と1994年にはドイツのマックス・プランクソフトウェアシステム研究所カイザースラウテルン大学で長期休暇を過ごしました。

参考文献

  1. ^ David A. Plaisted (1978).項書き換えシステムの停止性を証明するための再帰的に定義された順序付け(技術レポート). イリノイ大学コンピュータサイエンス学部. p. 52. R-78-943.
  2. ^バックメア、L.;プレイステッド、DA (1985)。ジャン=ピエール・ジュアンノー(編)。関連付けられたパスの順序付け。 LNCS。 Vol. 202.シュプリンガー・フェルラーク。241–54ページ 
  3. ^ David A. Plaisted (1981). 「抽象化による定理証明」Artif. Intell . 16 (1): 47–108 . doi : 10.1016/0004-3702(81)90015-1 .
  4. ^ David A. Plaisted (1982). 「簡略化された問題削減フォーマット」. Artif. Intell . 18 (2): 227–61 . doi : 10.1016/0004-3702(82)90041-8 .
  5. ^ Xumin Nie; David A. Plaisted (1989年1月).修正問題縮約形式の意味的変種(PDF) (技術レポート). ノースカロライナ大学チャペルヒル校. p. 11. TR89-101.
  6. ^ Jean H. Gallier、Paliath Narendran、David A. Plaisted、Stan Raatz、Wayne Snyder (1993). 「多項式時間で書換え規則の標準集合を見つけるアルゴリズム」(PDF) . J. ACM . 40 (1): 1– 16. doi : 10.1145/138027.138032 . S2CID 820591 . {{cite journal}}: CS1 maint: 複数の名前: 著者リスト (リンク)
  7. ^ David A. Plaisted; Steven Greenbaum (1986). 「構造を保持する節形式の翻訳」 . J. Symbolic Comput . 2 (3): 293– 304. doi : 10.1016/s0747-7171(86)80028-1 .
  8. ^ Jean H. Gallier; Paliath Narendran; David A. Plaisted; Wayne Snyder (1990). 「Rigid E-Unification: NP-Completeness and Applications to Equational Matings」 . Inf. Comput . 87 (1/2): 129–95 . doi : 10.1016/0890-5401(90)90061-l .
  9. ^ David A. Plaisted (1985). 「意味的合流性テストと補完法」 .情報制御. 65 (2/3): 182– 215. doi : 10.1016/s0019-9958(85)80005-x .
  10. ^ David A. Plaisted; Andrea Sattler-Klein (1996). 「等式完成のための証明の長さ」(PDF) . Inf. Comput . 125 (2): 154– 70. doi : 10.1006/inco.1996.0028 .
  11. ^ Shie-Jue Lee; David A. Plaisted (1994). 「定理証明における置換規則の利用」.コンピュータサイエンスにおける論理法. 1 (2): 217–40 .
  12. ^ Heng Chu; David A. Plaisted (1994). 「意味的に誘導されたインスタンスベース定理証明におけるモデル発見」. Fundam. Inform . 21 (3): 221– 235. doi : 10.3233/FI-1994-2134 .
  13. ^ Xumin Nie; David A. Plaisted (1990年7月). 「完全なセマンティックバックチェイニング証明システム」. ME Stickel (編). Proc. 10th CADE . LNAI. Vol. 449. Springer. pp.  16– 27.