一阶谓词逻辑（First-order predicate logic）是一种形式化的逻辑系统，用于描述和推理关于对象和它们之间关系的陈述。它是一种基于谓词和量词的逻辑系统，谓词用于描述对象之间的关系，量词用于描述对象的数量。

一阶谓词逻辑的语言包括常量、变量、谓词、量词和逻辑符号。常量是指具体的对象，如人、动物等；变量是指未指定具体对象的符号，如x、y等；谓词是指描述对象之间关系的符号，如“是父亲”、“大于”等；量词是指描述对象数量的符号，如“存在”、“所有”等；逻辑符号包括否定、合取、析取、条件、双条件等。

一阶谓词逻辑的推理方法包括演绎推理和归纳推理。演绎推理是从已知的前提出发，通过逻辑规则推导出结论的过程；归纳推理是从具体的实例中归纳出普遍规律的过程。

一阶谓词逻辑在人工智能、计算机科学、哲学等领域有广泛的应用，如知识表示、自然语言处理、形式化验证等。