Computational Logic Glossary

The use of computer programs to prove mathematical or logical theorems without human guidance.

An algebraic structure with operations AND, OR, and NOT over truth values, forming the basis of digital logic and propositional calculus.

A disjunction of literals used in conjunctive normal form (CNF) representations of logical formulas.

A property of a logical system guaranteeing that every valid formula can be derived through the proof rules.

A standard form for propositional formulas expressed as a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals.

The property of a problem for which an algorithm exists that always terminates with a correct yes or no answer.

A type whose definition depends on a value, enabling types to express precise program specifications.

A family of knowledge representation formalisms providing the logical foundation for ontology languages like OWL.

A semantic relationship where a set of premises logically guarantees the truth of a conclusion in every model.

A modal logic dealing with knowledge and belief operators for reasoning about what agents know or believe.

A formal logical system using quantifiers and predicates to express statements about objects and their relationships.

The process of mathematically proving that a system conforms to its specification.

A logical clause with at most one positive literal, forming the basis of logic programming languages like Prolog.

A syntactic transformation that derives new formulas from existing ones while preserving validity.

A formal system for expressing computation based on function abstraction and application, developed by Alonzo Church.

An atomic proposition or its negation, serving as the basic unit in clausal representations of formulas.

An interpretation that assigns meaning to the symbols of a logical language, providing a structure in which formulas are evaluated.

An automated technique that exhaustively explores the state space of a system to verify temporal logic properties.

A fundamental inference rule: from P and P implies Q, conclude Q.

An interactive software tool for developing and verifying formal mathematical proofs, such as Coq, Lean, or Isabelle.

A branch of logic dealing with propositions and logical connectives, where formulas are evaluated using truth values.

An inference rule that derives new clauses by eliminating complementary literals from two parent clauses.

A property of a logical system guaranteeing that every derivable formula is logically valid.

A family of logics with operators for reasoning about propositions qualified in terms of time.

An algorithm that finds a substitution making two logical terms syntactically identical, fundamental to automated deduction.