자동 추론 지침서

Handbook of Automated Reasoning

자동 추론 지침서(Automated Reasoning) ISBN044508139, 2128페이지)는 자동화된 추론 분야에 관한 조사기사를 모은 것이다.2001년 6월 MIT Press에 의해 출판된 이 책은 존 앨런 로빈슨과 안드레이 보론코프에 의해 편집되었다.제1권에서는 고전적 논리학, 평등과 다른 이론을 가진 1차 논리학, 그리고 유도를 기술하고 있다.제2권에는 고차, 비고급 및 기타 종류의 논리가 수록되어 있다.

색인

제1권

역사
고전 논리학
  1. 레오 바흐메어, 하랄트 간징거.해상도 정리 증명 페이지 19-99.
  2. 라이너 헨레표고 및 관련 방법, 페이지 100–178.
  3. 아나톨리 데그티아레프, 안드레이 보론코프.역법, 페이지 179–272.
  4. 마티아스 바아스, 우베 엘리, 알렉산더 리치.정규 형태 변환, 페이지 273–333.
  5. 안드레아스 노넨가르트 크리스토프 바이덴바흐소조항 정규 양식 계산, 페이지 335–367.
평등과 다른 이론
  1. 로버트 니우웬후이스 알베르토 루비오매개변수 기반 정리 증명, 페이지 371–443.
  2. 프란츠 바더, 웨인 스나이더.통일론, 445~532쪽.
  3. 나첨 더쇼위츠, 데이빗 플라우드.다시 쓰세요, 페이지 535–610.
  4. 아나톨리 데그티아레프, 안드레이 보론코프.Sequent-Based Calculi의 동등성 추론, 페이지 611–706.
  5. 상칭추, 샤오상가오.기하학에서의 자동 추론, 페이지 707–749.
  6. 알렉산더 보크마이어 볼커 위스페닝수치 제약 조건 해결, 페이지 751–842.
유도
  1. 앨런 번디수학적 유도에 의한 증명 자동화, 페이지 845–911.
  2. 휴버트 코몬.무유도 유도, 페이지 913–962.

제2권

고차 논리 및 논리 프레임워크
  1. 피터 B. 앤드류스.고전적 유형 이론, 페이지 965–1007.
  2. 길레스 다우크고차 통일과 매칭, 페이지 1009-1062.
  3. 프랭크 페닝.논리적 프레임워크, 페이지 1063–1147.
  4. Henk Barrendregt, Herman Geuvers. Henk Barendregt, Her종속형 시스템을 사용하는 증명 분석가, 페이지 1149–1238.
논클래식 로직스
  1. 위르겐 딕스, 울리히 푸르바흐, 일카 니에멜레.비모노토닉 추론:효율적인 계산 및 구현에 대하여, 페이지 1241–1354.
  2. 마티아스 바아즈, 크리스티안 페르뮐러, 제르노 살저다변량 로직 자동 공제 페이지 1355–1402.
  3. 한스 위르겐 올바흐, 안드레아스 노넨가르트, 마아텐 드 리케, 도브 가베이.고전적 로직에서 2-값 비고전적 로직 인코딩, 페이지 1403–1486.
  4. 아릴드 왈러비분류 로직의 연결, 페이지 1487–1578.
구분 가능한 클래스 및 모델 빌딩
  1. 디에고 칼바네세, 주세페 드 지아코모, 마우리치오 렌체리니, 다니엘레 나르디.표현 설명 로직에서의 추론, 페이지 1581–1634.
  2. 에드먼드 클라크, 홀거 슐링로프.모델 점검, 페이지 1635–1790.
  3. 크리스티안 페르뮐러, 알렉산더 리치, 울리히 휴스타트, 타넬 탐메트.결의안 결정 절차, 페이지 1791–1849.
실행
  1. IV 라마크리쉬난, R.세카르, 안드레이 보론코프용어 색인, 페이지 1853–1964.
  2. 크리스토프 바이덴바흐.중첩, 분류 및 분할 페이지 1965-2013.
  3. 라인홀드 레츠, 저노트 스텐즈모델 제거 및 연결 Tableau 절차, 페이지 2015–2114.

외부 링크