2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




 
 построить вывод формул в ИВ
Сообщение27.09.2008, 19:28 
Аватара пользователя
Помогите пожалуйста построить вывод формулы в исчислении высказываний:

\[
\left( {B \to C} \right) \to \left( {\left( {A \vee B} \right) \to \left( {A \vee C} \right)} \right)
\].

Аксиоматика такая:

\[
\begin{gathered}
  1.A \to \left( {B \to A} \right) \hfill \\
  2.\left( {A \to \left( {B \to C} \right)} \right) \to \left( {\left( {A \to B} \right) \to \left( {A \to C} \right)} \right) \hfill \\
  3.\left( {\neg B \to \neg A} \right) \to \left( {\left( {\neg B \to A} \right) \to B} \right) \hfill \\ 
\end{gathered} 
\]

Вообще, что значит построить вывод формулы? Я так понимаю, что, например, теорему дедукции использовать нельзя, потому что теорема дедукции дает некий критерий, когда формула выводима, но не строит сам вывод. А построить вывод, это значит использовать только аксиомы и правило вывода.

Правило вывода - modus ponens.

 
 
 [ 1 сообщение ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group