Formal Concept Analysis -also called Galois Lattices - is an algebraic model based on propositional calculus that is used for symbolic knowledge exploration from a formal context. The aim of this paper is to design the theoretical models required for the extension of Formal Concept Analysis to 1st order logic so as to improve both the expression power as a knowledge mining tool upon first order contexts, and the relevance of its results. But the design of the mathematical model represents a main interest by itself. Our contribution consists in: i) a synthesis of the basic notions of FCA, ii) the design of the Cube Model dedicated to the conjunctions of literals, iii) the design of a complete 1st-order logic formal concept analysis model. The approach is described from the theoretical point of view, implementations in logic programming and applications are also briefly presented.