Logic-ml

logic-ml@fos.kuis.kyoto-u.ac.jp

1792 discussions

CFP: PPL2015 第17回プログラミングおよびプログラミング言語ワークショップ論文募集
by Makoto Hamana 25 Sep '14

25 Sep '14

皆様、群馬大学の浜名と申します．来年3月に愛媛県松山市道後温泉で開催される第17回プログラミングおよびプログラミング言語ワークショップのご案内です．より詳細な投稿方法などは決定次第，下記ワークショップ Webページにてお知らせしますので，ぜひご投稿，ご参加をご検討ください． -------------------------------------------------------------------------- 第17回プログラミングおよびプログラミング言語ワークショップ（PPL2015） http://www-kb.is.s.u-tokyo.ac.jp/ppl2015/ 論文募集主催: 日本ソフトウェア科学会プログラミング論研究会日程: 2015年3月4日(水)〜3月6日(金) 会場: 愛媛県松山市道後温泉「道後プリンスホテル」 http://www.dogoprince.co.jp/ PPL2015は，プログラミングおよびプログラミング言語に関する研究者が一堂に会し，最新の研究成果の発表，および新たな研究課題についての討論やアイディア交換等を行うことを目的とした，合宿形式のワークショップです．プログラミングおよびプログラミング言語の理論・設計・実装・処理系などに関する研究発表を，カテゴリ別に幅広く募集します．カテゴリ1: 国内外で未発表の論文の発表カテゴリ2: 国際会議・学術雑誌等で既発表であるが，国内では未発表の研究の紹介カテゴリ3: ポスター・デモ発表（既発表・未発表の別を問いません）カテゴリ4【新規】: サーベイ・チュートリアルの発表（既発表・未発表の別を問いません）カテゴリ1の採択論文の中から，特に独創的なアイディアや顕著な成果を含むものに対して論文賞を授与する予定です．また全論文発表と全ポスター・デモのなかから，聴衆の投票によりそれぞれ，最も優秀な論文プレゼンテーションには発表賞（一般の部，学生の部．既受賞者は除く），最も優秀なポスター・デモにはポスター賞【新規】を授与する予定です．カテゴリ1（国内外未発表論文） ---------------------------- 完成した理論やシステムの研究発表のみならず，萌芽的なアイディアや問題点の提示等も歓迎します．発展途上の研究内容も積極的に採録する方針です（ただし，PPLでの発表として相応しくないと判断される場合は，この限りではありません）．また，カテゴリ1で発表された研究については，会場での討議や査読コメントをもとにその完成度を高め，将来の学術雑誌・会議等での業績に結び付けることを奨励しています．そのため，予稿集の配布は参加者のみへの限定的なものとする予定です．採録された論文は，PPL2015参加者に配布される予稿集に掲載され，参加者のみがアクセス可能な形でWeb上で公開されます（論文へのリンク集ページを作成し，閲覧に必要なパスワードを参加者に連絡します）．カテゴリ1で発表された研究のうち，PPL2015プログラム委員会により優れていると認めるものは，PPL2015終了後（2015年4月下旬予定），「コンピュータソフトウェア」誌のPPL2015推薦論文としての投稿が可能です．推薦論文は，PPL プログラム委員が引き続き査読を行うことによる，迅速な査読プロセスを特長としています．カテゴリ2（国外既発表論文） -------------------------- 査読付の国際会議または学術雑誌等で既発表であるが国内では未発表である研究を紹介する場です．採録決定済みの研究も含みます．PPLへの関連をもとに採否を判定いたしますが，申し込み多数の場合はプログラム委員会での選考により，発表をご遠慮いただく可能性もございますので，その旨をご了承の上ご投稿ください．カテゴリ3（ポスター・デモ発表） ------------------------------ 2時間程度のセッション内でのポスター発表またはデモ発表です．既発表・未発表の別を問いません．PPLへの関連をもとに採録を判定いたします．また，申し込み多数の場合はプログラム委員会での選考により採否を決定します． ※ショートプレゼンテーションは行いませんカテゴリ4（サーベイ・チュートリアル発表）【新規】 ------------------------------------------------ サーベイはプログラミング言語に関連するトピックについての(発表者の研究も含め)研究動向の紹介，チュートリアルはプログラミング言語に関連する基礎事項についての解説を募集します．既発表・未発表の別を問いません．プログラミング言語分野の学生，研究者の研究に役立つような発表を想定しています．分野間の相互理解と全体の底上げとなる事を期待し，新たに設置するものです．PPLへの関連および関連研究への言及をもとに採択を判定いたします．通常発表と同様の30分での発表を予定していますが，採択件数によっては発表者との相談で延長も考慮します． ====================================================================== 投稿・発表申込要領 4つのカテゴリそれぞれに対する投稿方法は以下の通りです．最新の情報は上記 Web ページでご確認ください．カテゴリ1（国内外未発表論文） ---------------------------- 投稿手続きは2段階です．発表申込を行った上で論文提出を行ってください．発表申込先： EasyChair による申込み受付を予定しています．発表申込締切：2014年12月22日(月) 17:00 (JST) 著者名，所属，論文タイトル，論文概要（日本語300〜400字程度もしくは英語 200 words 程度）を提出してください．論文提出締切：2015年1月8日(木) 17:00 (JST) 10ページ程度（最大15ページ）の論文（日本語もしくは英語，PDF形式）を提出してください．採否通知：2015年2月3日(火) 最終原稿提出締切：2015年2月16日(月) 17:00 (JST) 採録された論文の最終原稿の提出方法は，採否通知にてお知らせいたします． (注) カテゴリ1への投稿論文と類似の論文を，他の会議（予稿集を出版するもの）・論文誌などに同時投稿する場合は，査読の有無に関わらず，その旨を発表申込および論文提出の際に明記してください．PPLでは同時投稿の事実のみをもって論文を不採録とすることはありませんが，採否の決定に利用する場合があります（他の会議との重複を避けるため，発表内容についての条件付採録とすることもあります）．カテゴリ2（国外既発表論文） -------------------------- 発表申込時に採録が決定している国際会議および国際学術雑誌の発表論文が対象です．理論系だけではなく実装系の論文の投稿も歓迎いたします．発表申込方法につきましては PPL2015 の Web ページをご確認ください．発表申込締切：2015年1月23日(金) 17:00 (JST) 原論文（ページ数不問，PDF形式）とabstract（テキスト形式）を，著者名，所属，論文タイトル，原論文の出典（発表会議名，掲載済／予定の別等）と併せてご提出ください．採否通知：2015年2月5日(木) カテゴリ3（ポスター・デモ発表） ------------------------------------------ ポスター・デモの区別を行わずに募集いたします．デモを行う場合は，発表概要においてその旨をご説明ください．発表申込方法につきましては PPL2015 の Web ページをご確認ください．発表申込締切：2015年2月9日(月) 17:00 (JST) 希望する発表形態（ポスター・デモの別）を明記して，著者名，所属，発表タイトル，発表概要（200〜300字程度）をご提出ください．採否通知：2015年2月16日(月) カテゴリ4（サーベイ・チュートリアルの発表） ------------------------------------------ サーベイまたはチュートリアルの提案を募集いたします．発表申込み時に概要の提出を行ってください．概要の内容，PPLへの関連および関連研究への言及をもとに採録を判定いたします．発表申込締切：2015年1月23日(金) 17:00 (JST) 著者名，所属，発表タイトル，発表の概要 (1〜3ページ，PDF形式．目的，カバーする話題，想定する聴衆，必要な知識の記述を含むもの)をご提出ください．またもしその内容の既発表のサーベイ，チュートリアル，解説等があれば，その文書（ページ数不問，PDF形式），著者名，所属，タイトル，文書の出典（発表雑誌，掲載済／予定の別等）も併せてご提出ください．採否通知：2015年2月5日(木) 問い合わせ先：ppl2015-oc [at] kb.is.s.u-tokyo.ac.jp （[at]を@に置き換えてください） ====================================================================== プログラム委員会青戸等人東北大学浅田和之東京大学岩崎英哉電気通信大学鵜川始陽高知工科大学馬谷誠二京都大学 [プログラム共同委員長] 大岩寛産業技術総合研究所亀山幸義筑波大学河内谷清久仁日本IBM 久野靖筑波大学木村大輔国立情報学研究所宋剛秀神戸大学塚田武志 University of Oxford 中田景子 Tallinn University of Technology 浜名誠群馬大学 [プログラム共同委員長] 平井洋一 FireEye 平石拓京都大学藤田憲悦群馬大学星野直彦京都大学増原英彦東京工業大学渡部卓雄東京工業大学組織委員会松田一孝東京大学 [組織委員長] 浜名誠群馬大学 [プログラム共同委員長] 馬谷誠二京都大学 [プログラム共同委員長] 末永幸平京都大学上野雄大東北大学海野広志筑波大学木村大輔国立情報学研究所 [ポスターセッション幹事] --------------------------------------------------------------------------

1 0

数学会からのお知らせ
by shioya＠math.tsukuba.ac.jp 22 Sep '14

22 Sep '14

日本数学会数学基礎論および歴史分科会会員の皆様今週の数学会に関するお知らせが２件あります。（重複投稿をご容赦ください）１．台風16号への対応について２．プロジェクターの利用とバス便に関してよろしくお願いいたします。塩谷真弘（2014年度分科会連絡責任評議員） %%%%%%%%%%%%%%%%% １．台風16号への対応について以下の文書はWeb上　　　　　http://mathsoc.jp/meeting/hiroshima14sept/typhoon16.html でも公開しています。 2014年度秋季総合分科会における台風第16号への対応について　　　　　　　　　　　　　　　　　　　　　　　　　　　　　2014年9月21日会員各位台風第16号（フォンウォン）が西日本に接近しつつあります．日本数学会理事会では9月25日（木）から広島大学東広島キャンパスで開催されます秋季総合分科会への影響について懸念をしておりますが、まず以下のようにこの件に関わる広報、周知のチャンネルを確立しておきたいと思います．以下の対応が杞憂で終わってくれたらと祈っておりますが、念のために会員内で周知をお願いいたします．秋季総合分科会の開催に関して重要なお知らせは以下の手段によって会員にお知らせします．（１）スマートフォンでない携帯電話でも読めるページ　　　http://mathsoc.jp/i/ （２）大会の公式ページ　　　http://mathsoc.jp/meeting/hiroshima14sept/ また極めて重要なお知らせはニュースレターの号外でもご案内いたします．このとき同時に、講演者にも講演申し込みに際して登録されたアドレスにメールをお送りします．秋季総合分科会に参加される方は可能な限りActivation Systemからニュースレターの購読を選択してくださいますようお願いいたします．また台風の交通機関への影響により講演をキャンセルされる場合は、大会本部に電子メールアドレス　　program14sept(a)mathsoc.jp または電話番号 090-1791-3483　までご連絡ください．　　　　　　　　　　　　　　　　　　　　　　日本数学会理事長　舟木　直久 %%%%%%%%%%%%%%%%% ２．プロジェクターの利用とバス便に関してウェブページ http://mathsoc.jp/meeting/hiroshima14sept/news20140920.html に同様の告知が準備してあり、続報はこのページに記載することになっています。 (1) 講演に関するお願い：USBメモリに講演ファイルを入れてご持参ください． 9月19日まで広島大学総合科学部で日本分析化学会が開催されていましたが，会場の総合科学部の設備が最新の機器に対応していないせいもあり，コンピュータとプロジェクタの接続トラブルが頻繁に起こったとの報告がありました．（ノートパソコンのうちおおよそ9割以上は正常に接続されていますが，特に新しいコンピュータ，Mac，との接続トラブルが絶えなかったそうです．なお， HDMIケーブルは使用できません．）そのため，多くの会場では，USBメモリを使って予備のコンピュータに講演ファイルを移し，対応したとのことです．つきましては，可能な限り，次のことをお願いできないでしょうか？＊トラブルに備えて，講演ファイルをpdfファイル化し，USBメモリに入れてご持参　頂き，講演時にはUSBを携行してください．プロジェクタ接続に困難が生じたときに　予備機にUSBをつなぐことにより講演ができるようにするためです．　（ただしpdf ファイルに埋め込んだ動画の動作については保証しかねます．）　なお，ファイル名はプログラムの講演番号（2桁）から始めてご自分のお名前も入れて 01数学太郎.pdf 　のようにしてください．＊接続に不安がある方や，（追伸2）に記した接続上の注意に対応できない方は，　講演開始時間前や休憩時間に，実行委員会で用意するコンピュータに講演ファイル　を移し，そちらのコンピュータをご使用ください． (2) JR西条駅と広島大学を結ぶバス：小銭２９０円をご用意ください．日本数学会開催中，JR西条駅と広島大学を結ぶバスは，同時期に開催する他学会があるため，混雑することが予想されており，臨時バスが増発されます．バスの時刻表は下記URLに掲載されていますので，印刷してお持ちください．　　http://mathsoc.jp/meeting/hiroshima14sept/bus_timetable.pdf 講演会場である総合科学部の最寄りのバス停は「広大西口」であり，広島大学内の最初のバス停である「広大中央口」ではありません．また，西条駅から広島大学までのバス運賃は290円です．両替による混雑を避けるために，小銭をご用意いただければ幸いです．なおバスで利用できるICカードは PASPYとICOCAのみです（Suicaなど他のICカードはご利用になれません）．以上，どうぞ宜しくお願い申し上げます．　　　　　　　　　　　　　　　　　　秋季総合分科会実行委員長　作間　誠追伸1 学会開催直前の時期ですので，この件に関して個別にお問い合わせ頂きましても，ご対応はいたしかねますのでご了承ください．ただし、今後新たな注意事項がでてきましたら，ウェブページ http://mathsoc.jp/meeting/hiroshima14sept/news20140920.html を通して会員の皆様にお知らせする予定です．追伸2 （接続上の注意）＊HDMIケーブルには対応していません．こちらで準備したRGBケーブルをご使用ください．＊パソコンの解像度を1024 × 768に設定してください．＊液晶プロジェクターとパソコンは，ミニD-sub15ピンコネクタ（ピンが5本×3段の　通常のもの）で接続します．　パソコン側にメスコネクタがない場合，接続に必要なアダプタは各自ご持参ください．　薄型WindowsノートやMacを使用される方は，接続変換コネクタを必ずご持参ください．追伸3（パソコンとプロジェクターの不適合について　　　　　　　　　　　　　　　　　--接続トラブルに関する日本分析化学会からの連絡）多くのPCはプロジェクターに正しく信号が入り問題なく投影できましたが，いくつかのパソコンではトラブルが発生しています．その例を下記にしるしておきます． a.　最近のノートＰＣでは昔のVGA出力（D-sub15コネクタ）ではなくHDMIという規格のモニター出力のノートPCがあります．この場合はHDMIとD-sub15の変換コネクタを使うことになりますがこのようなケースでかなりの確率でプロジェクターへの出力がうまくいかないようです．またVGA出力（D-sub15コネクタ）とHDMIの両方をもつノートPC（例えばPanasonicのレッツノートのシリーズ）でもHDMI優先でVGAをまともに認識しないものがあるそうです. 有効な対策はないようで、別のPCへデータを移して映写する他ないようです． b.　MacBookAirの一部では時としてプロジェクターへ映写が大変暗くほとんど見えない程度にしか写らないことがあります（これはまれな現象です）．私の座長中にも1件発生し、いろいろやったのですが結果的にうまく映写することはできませんでした．しかし、これについては、Macがバッテリ駆動の時ではモニター出力信号が弱くなるためであり「ACアダプタを接続すると回避できる可能性がある」そうです． c.接触不良などの物理的な問題うまく写らない場合の一つの原因としてコネクタの接触不良もあるようです．差し直すとうまくいったとの話も何件かあったようです．Macのアダプタを差し直すとうまくいったとの話もありました．

1 0

再送：数学基礎論若手の会
by YOSHIDA Satoru 22 Sep '14

22 Sep '14

皆様重複して受け取られた場合はご容赦ください。数学基礎論若手の会2014のご案内です。数学基礎論を専攻する学生および若手研究者の研究交流を目的とする合宿形式の研究集会です．講演はオリジナルの成果発表に限らず，研究の途中報告や研究内容の紹介など幅広く募集しております．また，これから数学基礎論を勉強したいと思っている方のご参加も歓迎します．多くの方々のご参加およびご講演をお待ちしています．日程：11月19日（水）午後－21日（金）午前場所：鳥取市サイクリングターミナル砂丘の家（鳥取砂丘付近） http://www.city.tottori.lg.jp/www/contents/1198114185831/ 幹事：吉田聡（鳥取環境大学） satoru-y(a)kankyo-u.ac.jp ホームページ： http://misc.kankyo-u.ac.jp/~satoru-y/wakate14/ 今年度若手の会申込み要領については上記ホームページをご参照ください。 -- 吉田聡<YOSHIDA, Satoru> 鳥取環境大学

1 0

QIT31口頭発表締切延長
by NISHIMURA Harumichi 22 Sep '14

22 Sep '14

logic-mlの皆様，第31回量子情報技術研究会口頭発表申込の締切が 10月3日（金）に延長されました．詳しくは以下のご案内をご覧ください．ご応募のほどよろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道 ---------------------------------------------------------- 第31回量子情報技術研究会(QIT31) ※口頭講演の申込締切を10/3(金)まで延長しましたので，奮ってご応募ください．研究会の内容情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．第31回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2014年11月17日(月)～18日(火) 会場: 東北大学さくらホール (〒980-8577 仙台市青葉区片平２－１－１東北大学片平キャンパス内) 発表募集分野 (申し込み状況によっては査読の可能性あり) 量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．定員: 200名参加費: 事前振込み一般4,000円，学生1,000円 (当日会場払いは一般5,000円，学生2,000円) (懇親会は別途) 研究会参加申込要領参加申込は下記 Web にて受付けます： http://staff.aist.go.jp/s-kawabata/qit/ 講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，電子情報通信学会の Web システムを使用する予定．【口頭講演申込締切】 2014年10月3日(金) ※延長しました．なお，申込数が予定数に達した時点で締め切る場合があります．【ポスター講演申込締切】 2014年10月3日(金) 【予稿原稿提出締切】 2014年10月3日(金) 【参加申込締切】 2014年10月24日(金) 【問合せ先】枝松圭一 (東北大学電気通信研究所) 三森康義 (東北大学電気通信研究所) 吉田真人 (東北大学電気通信研究所) Email: qit31(a)quantum.riec.tohoku.ac.jp 主催: 量子情報技術時限研究専門委員会 (委員長: 枝松圭一 (東北大学)) 共催: 応用物理学会量子エレクトロニクス研究会東北大学電気通信研究所 ―――――――――――――――――――――――――――――

1 0

Prof. Aleksy Schubert at NII Logic Seminar
by Makoto Tatsuta 22 Sep '14

22 Sep '14

Prof. Aleksy Schubert at NII Logic Seminar Date: September 26, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 1716 (17th floor) 場所: 国立情報学研究所 17階 1716室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aleksy Schubert (University of Warsaw) (1) Title: Undecidability and complexity in fragments of first-order intuitionistic logic Abstract: In case of classical first-order logic there is a full characterisation of decidable and undecidable classes of formulae depending on the quantifier prefix and the vocabulary that is used. First-order logic in intuitionistic case lacks this kind of classification since there is no prefix normal form and actually the prenex fragment of the logic is in many cases much weaker than the general calculus. However, there is one meaningful stratification of the intuitionistic logic similar to the prenex form. We can consider classes of formulae that would result in a particular prefix of quantifiers when transformed using classical equivalences. The status of decidable and undecidable cases within this stratification will be presented as well as the complexity of known subcases. (2) Title: Verification of programs using Frama-C and Why3 Abstract: Frama-C is a tool that makes it possible to do a variety of analyses for C programs annotated with C specification language called ACSL (The ANSI/ISO C Specification Langage). One of the possible ways to use Frama-C is to generate verification conditions for appropriately defined Hoare logic that is in line with C programming language semantics. These verification conditions can subsequently be discharged by Why3 tool that makes it possible to manage the proving of necessary properties. During the talk I will present an overview of the tools and show a number of interesting examples to demonstrate how these tools work together to make possible verification of practical programs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内
by Yoshihito Tanaka 22 Sep '14

22 Sep '14

九州大学マス・フォア・インダストリ研究所の溝口先生の代理で投稿いたします． ========================================================================= 研究集会「高信頼な理論と実装のための定理証明および定理証明器」案内　　　　　　　　　　　　　　　　　　　(English version is below.) 12月3日(水)-5日(金)に九州大学西新プラザにて, 研究集会「高信頼な理論と実装のための定理証明および定理証明器」を開催します. 皆様のご参加をお待ちしています. 日時：2014年 12月3日(水) 〜 12月5日(金) 場所：九州大学・西新プラザ (福岡市早良区西新2-16-23) http://bit.ly/QdaiNishijin 福岡空港から地下鉄で西新駅まで約20分, その後, 徒歩約10分. プログラム：詳細は未定(準備中)です. みなさまのご講演をお待ちしています. Adam Chlipala氏 (MIT, USA), Cyril Cohen 氏 (Univ. Gothenburg, Sweden) をお招きして, Coqおよび Ssreflect, MathCompに関する御講演を頂く予定です. 参加者と講演の数を大体把握しておきたいと思いますので，参加される方は 10月半ばまでに下の参加申し込みを下記メールアドレスまでお送りください．参加者には，できるだけ講演していただければと思います．申込み・問い合わせ先: tpp2014(a)imi.kyushu-u.ac.jp (溝口佳寛(九州大学)) URL: http://coop-math.ism.ac.jp/event/2014E04 (注. 作成途中です.「TPP2014 数学」で検索してみて下さい.) ------------------------------------------------------------------------- TPP 2014 参加申し込みお名前：ご所属：講演　：する／しない懇親会：参加する／参加しない講演する場合タイトル：（講演のタイトルが決まっていなければ，TBAでもかまいません．決まったらご連絡ください．）講演希望日: (○/×) 12/3 (○/×) 12/4 (○/×) 12/5 その他(ご意見/ご要望ありましたらお願いします): ------------------------------------------------------------------------- ========================================================================= Workshop: Theorem proving and provers for reliable theory and implementations (TPP2014) This is the call for participation for TPP2014, to be held on Dec. 3(Wed) - 5(Fri), 2014 at Kyushu University. Date: 2014/12/03 around 1pm to 12/05 around 3pm Venue: Nishijin Plaza, Kyushu University (2-16-23 Nishijin, Sawara-ku, Fukuoka City) http://bit.ly/QdaiNishijinPDF Invited Speakers: Adam Chlipala (MIT, USA) Cyril Cohen (Univ. Gothenburg, Sweden) If you are planning to attend the meeting, please send the information slip below to the indicated address by mid-October. Submission/questions to: 　　　tpp2014(a)imi.kyushu-u.ac.jp (Yoshihiro Mizoguchi) URL: http://coop-math.ism.ac.jp/event/2014E04 (Tentative Japanese HP. Revised English HP will be notified later.) ------------------------------------------------------------------------- TPP 2014 Registration Name: Affiliation: Will give a talk: Yes/No Will attend the party: Yes/No Title of the talk: (If it is not decided yet, TBA is OK.) Which date do you prefer to talk ? 12/3 (OK/NG) 12/4 (OK/NG) 12/5 (OK/NG) Requests for the organizer (if any): ------------------------------------------------------------------------- =========================================================================

1 0

Prof. Aart Middeldorp at NII Logic Seminar
by Makoto Tatsuta 17 Sep '14

17 Sep '14

Prof. Aart Middeldorp at NII Logic Seminar Date: September 22, 2014, 14:00--16:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Aart Middeldorp (University of Innsbruck) Title: Proving AC Termination by Knuth-Bendix Orders Abstract: Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-founded orders that are compatible with the AC axioms. In this talk we consider various definitions of AC-compatible Knuth-Bendix orders. The orders of Steinbach and of Korovin and Voronkov are revisited. The former is enhanced to a more powerful AC-compatible order and we modify the latter to amend its lack of monotonicity on non-ground terms. We present new complexity results and compare the various orders on problems in termination and completion. The talk is based on joint work with Nao Hirokawa, Sarah Winkler, and Akihisa Yamada. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

JAIST Logic Seminar Series (18th Sep. 2014: Tadeusz Litak on Relational lattices)
by Katsuhiko Sano 14 Sep '14

14 Sep '14

皆様、 FAU Erlangen-Nürnberg の Tadeusz Litak さんの講演のお知らせです。ふるってご参加ください。問い合わせ先：佐野勝彦北陸先端科学技術大学院大学情報科学研究科 e-mail: v-sano(a)jaist.ac.jp ---------------------------------------------------------------------------------------------------- * JAIST Logic Seminar Series * Date: Thursday, 18th September, 2014, 15:10-17:00 Place: JAIST Collaboration Room 6 (I57-g) (Access:http://www.jaist.ac.jp/english/location/access.html) Speaker: Tadeusz Litak (Department Informatik, Technische Fakultät, FAU Erlangen-Nürnberg, Germany) Title: Relational lattices Abstract: We study an interpretation of lattice connectives as natural join and inner union between database relations with non-uniform headers. We show that this interpretation proposed by database experts (Vadim Tropashko from Oracle) yields a class of lattices which has not been considered in the existing lattice-theoretical literature. We discuss axiomatizability and decidability of their (quasi-)equational theory and propose an equational axiomatization for a corresponding abstract algebraic class. It turns out that addition of just the “header constant” to the lattice signature already allows mimicking the Maddux technique for cylindric algebras and encode the word problem for semigroups in the quasiequational theory. Relational lattices, however, are not as intangible as one may fear: for example, they do form a pseudoelementary class. We also apply the tools of Formal Concept Analysis and investigate standard contexts of relational lattices, obtaining, e.g., results on their subdirect irreducibility. This is a joint work with Szabolcs Mikulas and Jan Hidders ----------------------------------------------------------------------------------------------------

1 0

$B?t3X4pACO@%5%^!<%9%/!<%k(B 2014
by fuchino＠diamond.kobe-u.ac.jp 12 Sep '14

12 Sep '14

皆様他の場所での掲示で既に御存知のことと思いますが，今年の数学基礎論サマースクールが 9月16日(火)から 9月19日(金) にかけて神戸大学で開催されます．今年のテーマは集合論，特に強制法理論の入門です．詳しくは： http://kurt.scitec.kobe-u.ac.jp/~fuchino/set-theory2014/kisoron-summerschoo… をごらんください．参加費参加登録等は必要ありません．興味のある方はぜひ御参加ください．この集会のプログラム： http://kurt.scitec.kobe-u.ac.jp/~fuchino/set-theory2014/program-summerschl1… なお，9月18日(木) 18:00--20:00 に立食の懇親会を予定しております (子細については上のプログラムを御覧ください)．参加を御希望の方はサマースクールの最初の二日の間に参加登録と実費 (3000円) の支払をお願いします．懇親会のみに参加される方も歓迎します．ただし，その場合には，レストランへの人数の登録の関係上，私 fuchino(a)diamond.kobe-u.ac.jp と懇親会のアレンジメントを担当している酒井拓史さん hsakai(a)people.kobe-u.ac.jp の両方に，9月23日午後までにメールで御連絡ください． -- best regards Saka\'e Fuchino (渕野昌) ------------------------------------------------------------------------- Kobe University Graduate School of System Informatics Rokko-dai 1-1, Nada, Kobe 657-8501 Japan e-mail: fuchino(a)diamond.kobe-u.ac.jp web page: http://kurt.scitec.kobe-u.ac.jp/~fuchino/ -------------------------------------------------------------------------

1 0

CFP: JURISIN2014 〆切延長
by Satoshi Tojo 09 Sep '14

09 Sep '14

Apologies if you receive this CFP multiple times. -------------------------------------------- !!Deadline Extention!! Due to many requests, we will extend the deadline for Eighth International Workshop on Juris-informatics (JURISIN 2014). New Submission Deadline: September 17, 2014 Conference date: November 23 - 24, 2014 venue: Raiosha Building, Keio University Kanagawa, Japan Aims and Scope Juris-informatics is a new research area which studies legal issues from the perspective of informatics. The purpose of this workshop is to discuss both the fundamental and practical issues among people from the various backgrounds such as law, social science, information and intelligent technology, logic and philosophy, including the conventional "AI and law" area. We solicit unpublished papers on theories, technologies and applications on juris-informatics. Topics Relevant topics include, but are not limited to, the following: Model of legal reasoning Argumentation / Negotiation / Argumentation agent Legal term ontology Formal legal knowledge-base / Intelligent management of legal knowledge-base Translation of legal documents Information retrieval of legal texts Computer-aided law education Use of Informatics and AI in law Legal issues on ubiquitous computing / multi-agent system / the Internet Social implications of use of informatics and AI in law Natural language processing for legal knowledge Verification and validation of legal knowledge systems Any theories and technologies which is not directly related with juris-informatics but has a potential to contribute to this domain Bar Exam Competition This year, JURISIN invites participation in a legal information extraction and entailment competition. Previous conferences/workshops have not conducted such a shared task on a large legal data collection, so we hope that the 2014 workshop will help establish a major experimental effort in the legal information extraction/retrieval field. The motivation for the competition is to help create a research community of practice for the capture and use of legal information. Please visit the homepage of the bar exam competition. http://webdocs.cs.ualberta.ca/~miyoung2/jurisin_task/index.html Invited Speakers Bart Verheij (Stanford University/ University of Groningen) Riichiro Mizoguchi (Japan Advanced Institute of Science and Technology) Submissions: the submission site via EasyChair is now open. We welcome and encourage the submission of high quality, original papers, which are not simultaneously submitted for publication elsewhere except as a submission to JURIX 2014 (The 27th International Conference on Legal Knowledge and Information Systems). The double submission policy with JURIX 2014 is as follows: Papers being submitted both to JURISIN2014 and JURIX2014 must note this on the title page. A paper to be presented at JURISIN2014 must be withdrawn from JURIX2014 and vice versa according to the choice by the authors. If the authors do not follow this double submission policy, the paper by the authors will not be included in the proceedings of JURISIN 2014. Post Proceedings: Selected papers will be published via Springer Verlag LNAI. In addition, the authors have an opportunity to submit their full versions to the special issue of Journal of New Generation Computing. The detail will be announced soon. Workshop Chair Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Organizing Committee Members Katsumi Nitta, Tokyo Institute of Technology, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Sano, Japan Advanced Institute of Science and Technology(JAIST), Japan Advisory Committee Members Trevor Bench-Capon, The University of Liverpool, UK Tomas Gordon, Fraunfoher FOKUS, Germany Henry Prakken, University of Utrecht & Groningen, The Netherlands John Zeleznikow, Victoria University, Australia Robert Kowalski, Imperial College London, UK Kevin Ashley, University of Pittsburgh, USA Program Committee Members Satoshi Tojo, Japan Advanced Institute of Science and Technology(JAIST), Japan Tokuyasu Kakuta, Nagoya University, Japan Hanmin Jung, Korea Institute of Science and Technology Information(KISTI), Korea Minghui Xiong, Sun Yat-sen University, China Minghui Ma, Southwest University, China Nguyen Le Minh, Japan Advanced Institute of Science and Technology(JAIST), Japan Katsuhiko Toyama, Nagoya University, Japan Makoto Nakamura, Nagoya University, Japan Marina De Vos, University of Bath, UK Guido Governatori, NICTA, Australia Paulo Novais, University of Minho, Portugal Seiichiro Sakurai, Meiji Gakuin University, Japan Ken Satoh, National Institute of Informatics and Sokendai, Japan Thomas Ågotnes, University of Bergen, Norway Robert Kowalski, Imperial College London, UK Katsuhiko Sano, Japan Advanced Institute of Science and Technology(JAIST), Japan Katumi Nitta, Tokyo Institute of Technology, Japan Katie Atkinson, University of Liverpool, UK Philip T H Chung, Australasian Legal Information Institute (AustLII), Australia Masahiro Kozuka, Okayama University, Japan Fumihiko Takahashi, Meiji Gakuin University, Japan Baosheng Zhang, China University of Political Science and Law, China Akira Shimazu, Japan Advanced Institute of Science and Technology(JAIST), Japan Home page of JURISIN 2014 http://www.jaist.ac.jp/org/jurisin2014/ ------------------------------------------------------ Satoshi Tojo Japan Advanced Institute of Science and Technology (JAIST)

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml