Un autre champ d'application intéressant est celui de la demande croissante pour une puissance de déduction «enfouie» dans les systèmes. Les concepteurs de ces systèmes utilisent a priori tout le calcul des prédicats de premier ordre, mais on observe parfois a posteriori que les théories exprimées sont simples (par exemple, elles ont des modèles finis). En fait, il arrive que les utilisateurs choisissent le calcul des prédicats de premier ordre pour sa facilité d'expression (plus grande que celle de formalismes à modèles finis comme le calcul propositionnel) plus que pour la puissance des théories exprimables.
Ce champ d'application a suscité l'étude de démonstrateurs de théorèmes parfois dits «maigres» (lean en anglais). Ils privilégient la simplicité d'écriture, la lisibilité et la modifiabilité, en sacrifiant, éventuellement, la résolution des problèmes les plus complexes. Il est donc relativement facile de les instrumenter et de les étendre. Les démonstrateurs maigres exploitent intensivement le fait que les systèmes de programmation logique sont des démonstrateurs automatiques, même s'ils sont incomplets pour cause de stratégie efficace et de spécialisation pour un fragment du calcul des prédicats, ou incorrects pour cause d'absence de test d´occurrence*.
Toute la question est de savoir
comment programmer un démonstrateur automatique incomplet et incorrect
(un système de programmation logique)
pour en faire un démonstrateur complet et correct.
Des exemples de cette approche sont le 
(Prolog Technology Theorem Prover) [Stickel 88],
[Manthey et Bry 88],
[Beckert et Posegga 95, Beckert et Posegga 96, Fitting 98],
pour Prolog,
et le démonstrateur d'Amy Felty pour
Prolog [Felty et Miller 88, Felty 89].
Tous ces exemples ont en commun d'être des démonstrateurs plutôt simples
qui réemploient dans une grande mesure les capacités des systèmes sur
lesquels ils sont fondés.
Il faut enfin noter que des démonstrateurs «maigres» ont été conçus pour
différentes logiques, classiques, intuitionnistes ou modales,
alors que Prolog ou Prolog sont essentiellements des démonstrateurs,
imparfaits,
pour la logique intuitionniste.
Cela reflète pour la démonstration automatique ce que nous disions pour le
-calcul
(voir les sections
«Introduction»* --
et «La métaprogrammation»*) :
le -calcul (ou la logique) de niveau objet n'a aucune raison
d'être le même que celui (ou celle) du métalangage,
et pourtant,
il est possible de réutiliser pour les implémenter
l'implémentation du métalangage.
Un démonstrateur enfoui construit sur Prolog a été utilisé
pour rechercher les programmes d'une bibliothèque en les indexant
par une spécification [Rollins et Wing 91].
Une autre application, en cours d'étude, est la vérification que les
exigences en qualité de service
d'un programme mobile sont satisfaites par la spécification
d'un site où le programme tente de s'exécuter [Issarny et Bidan 96].
Une équipe du 
de Caen
(Service d'études communes de la Poste et de France Télécom)
modélise et implémente des agents
intelligents coopérants en Prolog [Beyssade et al. 95].
L'aspect concurrence est pris en compte par un autre langage que
Prolog,
et là encore l'ouverture
du système 
est importante.
Les agents disposent d'une puissance déductive enfouie,
leur «intelligence»,
qui leur permet de s'adapter au contexte et d'en rendre compte.
Par exemple,
dans un tel système,
on ne demande plus à imprimer tel document sur tel matériel,
mais on demande à un agent d'imprimer tel document.
À lui de trouver une imprimante adaptée et en service,
et éventuellement, de rendre compte de circonstances inhabituelles
(par exemple,
pas d'imprimante disponible, ou imprimante inhabituellement éloignée).
Ici,
la logique pour laquelle il faut implémenter un démonstrateur
enfoui est une logique modale.
En effet,
chaque agent a une vision du monde faite de croyances
(sur le monde et les autres agents)
et de certitudes.