명제 성 정리 입증

Question

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

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

도움 주셔서 감사합니다.

Answer 1

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

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