記号論理学の形式体系で、実際の普通のコンピュータ(チューリングマシン)に対応してるものってどれですか? 命題論理とか、一階述語論理とか