2011-11-24 2 views
2

명제 정리 증명을위한 전략으로 폭스 우선 검색을 사용할 수 있습니까? (나는 명확한 문제 공식을 볼 수 없습니다 : 각 주에서 사용할 수있는 행동은 무엇이며 어떤 주가 무엇인지).명제 성 정리 입증

나는 그물에서 어디에서나 설명을 찾고있었습니다. 모든 문서에는 BFS가 언급되어 있지만 그 중 어느 것도 알고리즘을 제공하지 않습니다.

도움 주셔서 감사합니다.

+0

달성하고자하는 것에 대해 더 자세히 설명해 주시겠습니까? '명제 정리 증명 (Propositional theorem proving)'은 상당히 거대한 영역이며 거의 제로에 가까운 세부 사항을 부여했습니다. – Gian

답변

1

상태는 파생어 목록입니다. 상태에서 상태로의 전환은 각 전제가 파생 목록에 결론으로 ​​나타나고 새 파생으로 목록을 확장하는 추론 규칙을 적용합니다.

이러한 상태와 전환을 사용하면 원하는 결론을 내릴 때까지 일반적인 BFS를 수행 할 수 있습니다.

+0

답장을 보내 주셔서 감사합니다. 구체적인 예나 튜토리얼에 대한 링크를 줄 수 있습니까? – saadtaame

+0

"앞으로 묶는 것"으로 검색하십시오. – namin

+0

앞으로 체인! 연결이 뭐야?! – saadtaame