Focalisation

Une discipline en théorie des preuves qui structure la recherche de preuves en phases alternées de « focalisation » déterministe et de « défocalisation » nondéterministe, regroupant des étapes d'inférence inversibles ou synchrones pour réduire la redondance et le branchement.