first-order-logic.hashnode.devUnderstanding Herbrand LogicWhen we write logic programs, what are we actually talking about? Herbrand Logic provides the semantic framework for understanding systems like Prolog. Vocabulary and Terms In Herbrand logic, our "universe" isn't made of physical objects, but of the ...Jan 6·3 min read
first-order-logic.hashnode.devA Beginner's Guide to Prolog Syntax and RecursionProlog (Programming in Logic) is unique because it lacks standard keywords like for or while. Instead, we define a knowledge base of facts and rules and ask questions about them. Syntax Basics Constants: Start with lowercase letters (e.g., john, piz...Jan 6·2 min read
first-order-logic.hashnode.devFrom Logic to Prolog: Horn Clauses and SLD-ResolutionHow do we bridge the gap between abstract mathematical resolution and a programming language like Prolog? The answer lies in a specific subset of logic called Horn Clauses. What is a Horn Clause? A Horn clause is a disjunction of literals with at mos...Jan 6·2 min read
first-order-logic.hashnode.devThe Resolution Proof MethodLogic programming and automated reasoning systems heavily rely on a proof technique called Resolution. Unlike natural deduction, which can feel like guesswork, resolution is a refutation procedure -- it tries to prove a formula is unsatisfiable. The ...Jan 6·2 min read
first-order-logic.hashnode.devPreparing Logic for Machines: PNF and SkolemizationIn the world of automated theorem proving, raw logical formulas are often too messy for algorithms to handle directly. Before a computer can prove a theorem, we usually need to standardize the format. Today, we look at two critical transformation ste...Jan 6·2 min read