Arboles de Forzamiento Sem\'antico para la Logica de Predicados

TL;DR

This paper introduces semantic forcing trees as a visual inference method for first-order predicate logic, linking their validity to standard valuation semantics and providing a way to refute invalid formulas.

Contribution

It presents semantic forcing trees as a novel visual inference tool that characterizes model semantics for first-order predicate logic.

Findings

Semantic forcing trees match standard valuation semantics for validity.

Refutation of invalid formulas is achieved through leaf markings in the trees.

The approach offers a visual and intuitive understanding of logical validity.

Abstract

Model semantics for first-order predicate logic is characterized by a visual inference tool called semantic forcing trees for predicate logic. Formulas that are valid (or invalid) by semantic forcing trees match valid (or invalid) formulas by the usual valuation semantics. In the event that the formula is invalid by a forcing tree, a model that refutes it is determined by the marks of the leaves of this tree.