| ||||||||||||||||||||||||
[Bur11a] Consistency Implies Cut AdmissibilityConférences Internationales sans actes : International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Wroclaw, Poland,Mots clés: automated theorem proving,proof theory,rewriting,deduction modulo,resolution
Résumé:
For any finite and consistent first-order theory, we can find a presentation as a rewriting system that enjoys cut admissibility.
Commentaires:
http://hal.inria.fr/view_by_stamp.php?&halsid=81q2577o677m66fuaa9bh79t37&label=PSATTT11&langue=en&action_todo=view&id=inria-00614040&version=1
Equipe:
sys
BibTeX
|
||||||||||||||||||||||||