La metodología y marco de ingeniería del conocimiento lógico-pluralista se aplica al modelado de una teoría de equilibrio legal, en la que el conocimiento legal (casos y leyes) se codifica utilizando preferencias de valores dependientes del contexto. La teoría obtenida se utiliza luego para formalizar, evaluar automáticamente y reconstruir casos ilustrativos de derecho de propiedad (que involucran la apropiación de animales salvajes) dentro del sistema de asistente de pruebas, ilustrando cómo se puede aprovechar la tecnología interactiva y automatizada de demostración de teoremas para proporcionar un banco de pruebas para el desarrollo y verificación formal de lenguajes y teorías legales específicos de dominio. Modelando el razonamiento legal orientado a valores en ese marco, establecemos puentes novedosos entre la última investigación en representación y razonamiento del conocimiento en lógicas no clásicas, demostración automática de teoremas y aplicaciones en el razonamiento legal.