コンピュータ科学では、分離論理はプログラムに関する推論の方法であるHoare論理の拡張です。これはJohn C. Reynolds、Peter O'Hearn、Samin Ishtiaq、およびHongsong Yangによって開発され、Rod Burstallによる初期の作業を描いています。分離ロジックのアサーション言語は、束縛された意味（BI）の論理の特殊なケースです。