التأويل (بالإنجليزية: interpretation) إسناد معنى الرموز في لغة متصرفة. تُعرّف العديد من اللغات الشكلية المستخدمة في الرياضيات والمنطق وعلم الحاسوب النظري بـ «مصطلحات نحوية» فقط، وبالتالي ليس لها أي معنى حتى تُفسر بطريقة محددة. تسمى الدراسة العامة لتفسيرات اللغات الشكلية باسم «الدلالات الشكلية».
المنطق الشكلي الأكثر شيوعًا هو «منطق القضايا» و«منطق المسندات» و«منطق الموجهات» النظير لهما، وهناك طرق قياسية لتقديم ترجمة تفسيرية لكل منها. في هذه السياقات، الترجمة التفسيرية هي عبارة عن دالة توفر امتدادًا لرموز وسلاسل الرموز لإحداى «لغات الهدف». على سبيل المثال، يمكن أن تستقبل دالة الترجمة التفسيرية «الدالة الخبرية» تي T (كرمز لـ «الطول») وتعين الامتداد {إيه a} (كرمز لـ «ابراهام لنكون»). لاحظ أن وظيفة الترجمة التفسيرية الخاصة بنا هو تعيين الامتداد {إيه a} للثابت غير المنطقي تي T، ولا تدعي ما إذا كان تي T يرمز للطول أو إيه a لابراهام لنكولن. ولا علاقة للترجمة التفسيرية المنطقية بالـ «روابط المنطقية» مثل «و and» و«أو or» و« ليس not». على الرغم من أننا قد نستخدم هذه الرموز للدلالة على أشياء أو مفاهيم معينة، إلا أن هذا لا يُحدد بواسطة دالة الترجمة التفسيرية.
غالبًا (ولكن ليس دائمًا) ما توفر الترجمة التفسيرية طريقة لتحديد «القيم الحقيقة» للجمل في اللغة. إذا كان الترجمة التفسيرية تحدد قيمة صحيحة إلى جملة أو نظرية، تُسمى الترجمة التفسيرية في هذه الحالة نموذج تلك الجملة أو النظرية.