Page 347 of 800
| Page 347 of 800 | Search internet |
The Peano page defines Peano arithmetic 
on top of First Order Predicate Calculus 
and defines on top of Propositional Calculus 
:
We refer to and theories like which include as first order theories. The Peano page assigns the FOL tactic 
to and . In general, the FOL tactic can be used with arbitrary first order theories.
Theories which build on but not on can use 
instead. The Prop tactic is like the FOL tactic but cannot handle quantifiers.
The FOL tactic allows to state proofs in a style which is convenient in connection with first order theories. The tactic translates FOL proofs into sequent proofs and may be seen as an implementation of a high level proof language on top of the low level sequent proof language.
| Page 347 of 800 | Search logiweb.eu |